constructing birestrictions with specific jectivities

• Its injectivity : \(\forall x\in I.\forall y\in I.(f(x)=f(y)\implies x=y).\)
• Its surjectivity : \(\forall y\in J.\exists x\in I.f(x)=y.\)
• Its bijectivity : its simultaneous injectivity and surjectivity.
• It being neither.

Proof    \(f\big|_\varnothing^\varnothing\) is of type \(\varnothing\to\varnothing.\) Thus, it's injective if and only if : $$\forall x\in\varnothing.\forall y\in\varnothing.(f(x)=f(y)\implies x=y)$$ This is true by principle of explosion. Likewise, it's surjective if and only if : $$\forall y\in\varnothing.\exists x\in\varnothing.f(x)=y$$ This is also true by principle of explosion. It is therefore both injective and surjective, thus proving its bijectivity. \(\blacksquare\)

Proof    \(f\big|_\varnothing^{\{*\}}\) is of type \(\{*\}\to\varnothing.\) Thus, it's injective if and only if : $$\forall x\in\varnothing.\forall y\in\varnothing.(f(x)=f(y)\implies x=y)$$ This is true by principle of explosion. Likewise, it's surjective if and only if : $$\forall y\in\{*\}.\exists x\in\varnothing.f(x)=y$$ However, \(\exists x\in\varnothing.f(x)=*\) is always false, which means it's always always non-surjective. \(\blacksquare\)

Proof    By algebraic manipulation, \begin{equation*} \begin{split} &\neg\forall x\in I.\forall y\in I.(f(x)=f(y)\implies x=y)\\ \dashv\vdash &\exists x\in I.\neg\forall y\in I.(f(x)=f(y)\implies x=y)\text{ by conversion of quantifiers}\\ \dashv\vdash &\exists x\in I.\exists y\in I.\neg(f(x)=f(y)\implies x=y)\text{ by }\!\!\left\{\!\!\begin{array}{ll}\text{conversion of quantifiers}\\\text{covariance of existential sentences' last components}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.\neg(\neg f(x)=f(y)\vee x=y)\text{ by }\!\!\left\{\!\!\begin{array}{ll}\text{material implication}\\\text{contravariance of negated components}\\\text{covariance of existential sentences' last components}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(\neg\neg f(x)=f(y)\land\neg x=y)\text{ by }\!\!\left\{\!\!\begin{array}{ll}\text{De Morgan laws}\\\text{covariance of existential sentences' last components}\\\text{covariance of conjunctions' components}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(f(x)=f(y)\land\neg x=y)\text{ by }\!\!\left\{\!\!\begin{array}{ll}\text{double negation elimination}\\\text{covariance of existential sentences' last components}\\\text{covariance of conjunctions' components}\end{array}\right.\\ \dashv\vdash &\exists x\in I.\exists y\in I.(\neg x=y\land f(x)=f(y))\text{ by }\!\!\left\{\!\!\begin{array}{ll}\text{commutativity of conjunction}\\\text{covariance of existential sentences' last components}\end{array}\right. \end{split} \end{equation*} Let \(x,y\in I\) such that \(\neg x=y\) and \(f(x)=f(y).\) If we define \(*:=f(x)=f(y)\in J,\) this ensures \(f^{-1}(\{*\})\) has at least two distinct elements, \(x\) and \(y.\) Therefore, \(|f^{-1}(\{*\})|\ge2.\) \(\blacksquare\)

Proof    \(f\big|_{\{x,y\}}^{\{*\}}\) is non-injective, as \(f(x)=*=f(y)\) while \(x\ne y.\) However, it is surjective, because its image \(f\big|_{\{x,y\}}^{\{*\}}(\{x,y\})=\{f(x),f(y)\}=\{*\}\) is its codomain. \(\blacksquare\)

Proof    \(f\big|_{\{x,y\}}^{\{*\}}\) is non-injective, as \(f(x)=*=f(y)\) while \(x\ne y.\) It isn't surjective either, because \(f\big|_{\{x,y\}}^{\{*,\{*\}\}}(\{x,y\})=\{f(x),f(y)\}=\{*\}\) is a proper subset of its codomain \(\{*,\{*\}\},\) as \({*}\ne\{*\}\) due to an infamous corollary of the axiom of regularity.

• It's bijective with \(I=\varnothing\) and \(J=\varnothing,\)
• It's injective non-surjective with \(I=\varnothing\) and \(J=\{*\},\)
• It's surjective non-injective with \(I=\{-\pi,\pi\}\) and \(J=\{\pi^2\},\)
• It's neither with \(I=\{-\pi,\pi\}\) and \(J=\{\pi^2,\{\pi^2\}\}.\)

• \(|I_0|\ge0\) and \(|J_0|\ge0\) for bijective birestrictions.
• \(|I_0|\ge0\) and \(|J_0|\ge1\) for injective non-surjective birestrictions,
• \(|I_0|\ge2\) and \(|J_0|\ge1\) for surjective non-injective birestrictions,
• \(|I_0|\ge2\) and \(|J_0|\ge2\) for non-injective non-surjective birestrictions.

Proof

• Every set has cardinality at least 0, which trivialises the first assertion. Using \(I_0=J_0=\varnothing\) always works as bijective birestriction, thanks to theorem 1.1. \(\Box\)
• By law of excluded middle, \(|I_0|\ne0\) or \(|I_0|=0.\) If \(|I_0|\ne0,\) then \(|J_0|\ne0\) because there is no map from a non-empty set to the empty set. If \(|I_0|=0\) and \(|J_0|=0,\) then \(I_0=J_0=\varnothing,\) which yields a bijective birestricted map which, therefore, isn't non-surjective ; hence, if \(|I_0|=0,\) we have \(|J_0|\ne0.\) By disjunction elimination, we have that \(|J_0|\ne0,\) or in other words, \(|J_0|\ge1.\) \(\Box\)
• By lemma 1.3, the non-injectivity of \(f\big|_{I_0}^{J_0}\) requires the existence of \(*\in J_0,\) thus \(|J_0|\ge1,\) such that \(\big(f\big|_{I_0}^{J_0}\big)^{-1}(\{*\})\) has at least two distinct elements. Since \(\big(f\big|_{I_0}^{J_0}\big)^{-1}(\{*\})\) is, by definition, a subset of \(I_0,\) we have that \(I_0\) also has at least two distinct elements, precisely the same ones ; thus \(|I_0|\ge2.\) All in all, we have that \(|I_0|\ge2\) and \(|J_0|\ge1.\) \(\Box\)
• As proved in the previous point, the non-injectivity of \(f\big|_{I_0}^{J_0}\) requires \(|I_0|\ge2\) and \(|J_0|\ge1.\) However, if \(|I_0|\ge2\) and \(|J_0|=1,\) then if you take any \({!}\in I_0,\) we indeed have that for all \(*\in J_0,\) we have \(f(!)=*,\) which proves its surjectivity. If we want it to be neither injective nor surjective, we must therefore have \(|J_0|\ge2.\) All in all, this means such a map birestriction has to be such that \(|I_0|\ge2\) and \(|J_0|\ge2.\) \(\blacksquare\)

Proof    By definition, \(f(I)\) is the set of all images of elements of \(I\) by \(f,\) which therefore guarantees surjectivity. \(\blacksquare\)

Proof    By non-injectivity of \(f,\) there exist \(x,y\in I\) such that \(x\ne y\) and \(f(x)=f(y).\) Then, \(f\big|_I^{f(I)}(x)=f\big|_I^{f(I)}(y),\) despite \(x\ne y,\) which proves its non-injectivity. \(\blacksquare\)

Proof    \(f\big|_I^{f(I)}\) is already non-injective surjective thanks to theorem 1.8, but \(f(I)\not\in f(I)\) by a corollary of the axiom of regularity, so \(f\big|_I^{f(I)\cup\{f(I)\}}\) is neither injective nor surjective. \(\blacksquare\)