avewright/proofwiki-math huggingface dataset:
Theorem: Count of Subsets with Odd Cardinality

Let $S$ be a set whose cardinality is $n$.
Then the number of subsets of $S$ whose cardinality is odd is $2^{n-1}$.

Proof:
Proof by induction:
For all $n \in \N$, let $\map P n$ be the proposition:
:The number of subsets of $S$ whose cardinality is odd is $2^{n - 1}$, where $\card S = n$.
=== Basis for the Induction ===
When $n = 1$ we have from Cardinality of Power Set of Finite Set that $S$ has $2^1 = 2$ subsets: $\O$ and $S$ itself.
We have that $\card S = 1$ and $\card \O = 0$.
So there is indeed $2^{1 - 1} = 2^0 = 1$ subset of $S$ whose cardinality is odd, and that is $S$.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:The number of subsets of $S$ whose cardinality is odd is $2^{k - 1}$, where $\card S = k$.
Then we need to show:
:The number of subsets of $S$ whose cardinality is odd is $2^k$, where $\card S = k + 1$.
=== Induction Step ===
This is our induction step:
Let $\card S = k + 1$.
Let $x \in S$.
Consider the set $S' = S \setminus \set x$.
We see that $\card {S'} = k$.
Let $A \subseteq S$.
If $x \notin A$ then $A \subseteq S'$.
If $x \in A$ then there exists a unique $A' \subseteq S'$ such that $A' \cup \set x = A$.
In fact, $A' = A \setminus \set x$.
Let $K$ be the number of subsets of $S'$ with an odd number of elements.
From the induction hypothesis we have that $K = 2^{k - 1}$.
Now adjoin $x$ to all the subsets of $S'$.
Suppose $E' \subseteq S'$, where $E'$ has an even number of elements.
Then $E' \cup \set x$ has an odd number of elements.
Similarly, $O' \subseteq S'$, where $O'$ has an odd number of elements.
Then $O' \cup \set x$ has an even number of elements.
So the number of subsets of $S$ with an odd number of elements is:
:$K$ subsets of $S$ that have an odd number of elements and are subsets of $S'$
and:
:$K$ subsets of $S$ of the form $O' \cup \set x$.
We have that subset $A$ of $S$ has a unique expression of the form $A'$ or $A' \cup \set x$ with $A' \subseteq S'$.
Thus there are exactly $2 K$ subsets of $S$ with an odd number of elements.
But as $K = 2^{k - 1}$ it follows that $2 K = 2^k$.
That is, there are $2^k$ subsets of $S$ with an odd number of elements.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
::The number of subsets of $S$ whose cardinality is odd is $2^{n - 1}$, where $\card S = n$.
{{qed}}
Theorem: Strictly Well-Founded Relation determines Strictly Minimal Elements

Let $A$ be a class.
Let $\RR$ be a strictly well-founded relation on $A$.
Let $B$ be a nonempty class such that $B \subseteq A$.
Then $B$ has a strictly minimal element under $\RR$.

Proof:
{{NotZFC}}
First a lemma:
Theorem: Category of Ordered Sets has Enough Constants

Let $\mathbf{OrdSet}$ be the category of ordered sets.
Then $\mathbf{OrdSet}$ has enough constants.

Proof:
By Singleton Ordered Set is Terminal Object, we have that any ordered set with a singleton as underlying set is terminal in $\mathbf{OrdSet}$.
Let $1$ be such a singleton ordered set.
To show that $\mathbf{OrdSet}$ has enough constants, it is to be shown that if:
:$f: P \to Q \ne g: P \to Q$
then there exists an $x: 1 \to P$ such that $f \circ x \ne g \circ x$.
Now by definition of $\mathbf{OrdSet}$, $f$ and $g$ are increasing mappings.
In particular, they are mappings, and by Equality of Mappings, there must be a $p \in P$ such that:
:$\map f p \ne \map g p$
Define $\bar p: 1 \to P$ by $\map {\bar p} * = p$ (where $*$ is the unique element of $1$).
If this is a morphism in $\mathbf{OrdSet}$, we are evidently done.
This follows from Mapping is Constant iff Increasing and Decreasing.
Hence $\mathbf{OrdSet}$ has enough constants.
{{qed}}
Theorem: Unique Constant in Category of Monoids

Let $\mathbf{Mon}$ be the category of monoids.
Then every object $M$ of $\mathbf{Mon}$ has precisely one constant.

Proof:
From Trivial Monoid is Terminal Element, we obtain that a constant of $M$ is a morphism $f: \left\{{e}\right\} \to M$.
By Trivial Monoid is Initial Element, there is precisely one such morphism.
Hence $M$ has one constant.
{{qed}}
Theorem: Well-Founded Induction

Let $\struct {A, \RR}$ be a strictly well-founded relation.
Let $\RR^{-1} \sqbrk x$ denote the preimage of $x$ for each $x \in A$.
Let $B$ be a class such that $B \subseteq A$.
Suppose that:
:$(1): \quad \forall x \in A: \paren {\RR^{-1} \sqbrk x \subseteq B \implies x \in B}$
Then:
:$A = B$
That is, if a property passes from the preimage of $x$ to $x$, then this property is true for all $x \in A$.

Proof:
{{AimForCont}} $A \nsubseteq B$.
Then:
:$A \setminus B \ne 0$
By Strictly Well-Founded Relation determines Strictly Minimal Elements, $A \setminus B$ must have some strictly minimal element under $\RR$.
Let $\map \complement B$ be the set complement of $B$.
Then:
{{begin-eqn}}
{{eqn | q = \exists x \in A \setminus B
      | l = \paren {A \setminus B} \cap \RR^{-1} \sqbrk x
      | r = \O
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cap \map \complement B} \cap \RR^{-1} \sqbrk x
      | r = \O
      | c = {{Defof|Set Complement}}
}}
{{eqn | ll= \leadsto
      | l = A \cap \paren {\map \complement B \cap \RR^{-1} \sqbrk x }
      | r = \O
      | c = Intersection is Associative
}}
{{eqn | ll= \leadsto
      | l = A \cap \paren {\RR^{-1} \sqbrk x \cap \map \complement B }
      | r = \O
      | c = Intersection is Commutative
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cap \RR^{-1} \sqbrk x } \cap \map \complement B
      | r = \O
      | c = Intersection is Associative
}}
{{end-eqn}}
So, by Intersection with Complement is Empty iff Subset:
:$A \cap \RR^{-1} \sqbrk x \subseteq B$
Since $\RR^{-1} \sqbrk x \subseteq A$, by definition of a subset:
:$\RR^{-1} \sqbrk x \subseteq B$
Thus, {{hypothesis}} $(1)$:
:$x \in B$
But this contradicts the fact that:
:$x \in A \setminus B$
By Proof by Contradiction it follows that:
:$A \setminus B = \O$
and so:
:$A \subseteq B$
Therefore:
:$A = B$
{{qed}}
Theorem: Cardinal Number is Ordinal

Let $S$ be a set such that $S \sim x$ for some ordinal $x$.
Let $\card S$ denote the cardinality of $S$.
Then:
:$\card S \in \On$
where $\On$ denotes the class of all ordinals.

Proof:
If $S \sim x$, then $\set {x \in \On: S \sim x}$ is a non-empty set of ordinals.
It follows that this set has a minimal element, its intersection.
{{explain|Needs a link to the fact that $\set {x \in \On: S \sim x}$ is the subset of a well-ordered set, and also that the intersection is that minimal element.}}
This minimal element is the cardinal number of $S$, by the definition of cardinal number.
Thus, it is an ordinal.
{{qed}}
Theorem: Condition for Set Equivalent to Cardinal Number

Let $S$ be a set.
Let $\card S$ denote the cardinality of $S$.
That is, let $\card S$ be the intersection of all ordinals equivalent to $S$.
{{ExtractTheorem|This following statement needs to go somewhere else as it's a non-sequitur in this context.}}
Note that in the absence of the Axiom of Choice, $\card S$ may be the class of all sets.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$S \sim \card S$}}
{{item|(2):|$\exists x \in \On: S \sim x$}}
{{item|(3):|$\exists x \in \On: \exists y: \paren {y \subseteq x \land S \sim y}$}}
{{end-itemize}}
where $A \sim B$ means that there is a bijection from $A$ onto $B$, and the quantification over $y$ is unbounded (so $y$ may be any set).

Proof:
=== $(2) \implies (1)$ ===
If $\exists x \in \On: S \sim x$, then by Class of All Ordinals is Well-Ordered by Subset Relation there is a smallest ordinal $x$ such that $S \sim x$.
This smallest ordinal $x$ is the cardinal number of $S$, by definition.
{{qed|lemma}}
Theorem: Cardinal Number Equivalence or Equal to Universe

Let $S$ be a set.
Let $\card S$ denote the cardinal number of $S$.
Let $\mathbb U$ denote the universal class.
Then:
:$S \sim \card S \lor \card S = \mathbb U$

Proof:
By Condition for Set Equivalent to Cardinal Number:
If $\exists x \in \On: S \sim x$, then:
:$S \sim \card S$
If $\neg \exists x \in \On: S \sim x$, then:
{{begin-eqn}}
{{eqn | l = \bigcap \set {x \in \On : S \sim x}
      | r = \bigcap \O
      | c = 
}}
{{eqn | r = \mathbb U
      | c = Intersection of Empty Set
}}
{{end-eqn}}
And thus by the definition of cardinal number:
:$\card S = \mathbb U$
{{qed}}
Theorem: Ordinal Number Equivalent to Cardinal Number

Let $x$ be an ordinal.
Let $\card x$ denote the cardinal number of $x$.
Then:
:$x \sim \card x$
where $\sim$ denotes set equivalence.

Proof:
From Set is Equivalent to Itself:
:$x \sim x$
Therefore, $x$ is equivalent to some ordinal.
By Condition for Set Equivalent to Cardinal Number:
:$x \sim \card x$
{{qed}}
Theorem: Cardinal Number Less than Ordinal

Let $S$ be a set.
Let $\card S$ denote the cardinal number of $S$.
Let $x$ be an ordinal such that $S \sim x$.
Then:
:$\card S \le x$

Proof:
Since $S \sim x$, it follows that:
: $x \in \set {y \in \On : S \sim y}$
By Intersection is Subset: General Result, it follows that:
: $\ds \bigcap \set {y \in \On: S \sim y} \subseteq x$
{{explain|Link to the fact that $\le$ is isomorphic to $\subseteq$ on ordinals.}}
Therefore $\card S \le x$ by the definition of cardinal number.
{{qed}}
Theorem: Equivalent Sets have Equal Cardinal Numbers

Let $S$ and $T$ be sets.
Let $\card S$ denote the cardinal number of $S$.
Then:
:$S \sim T \implies \card S = \card T$

Proof:
Let $x$ be an arbitrary set that is an ordinal:
{{begin-eqn}}
{{eqn | l = S
      | o = \sim
      | r = T
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = S \sim x
      | o = \iff
      | r = T \sim x
      | c = Set Equivalence behaves like Equivalence Relation
}}
{{eqn | ll= \leadsto
      | l = \set {x \in \On : S \sim x}
      | r = \set {x \in \On : T \sim x}
      | c = {{Defof|Class Equality}}
}}
{{eqn | ll= \leadsto
      | l = \bigcap \set {x \in \On : S \sim x}
      | r = \bigcap \set {x \in \On : T \sim x}
      | c = Substitutivity of Class Equality
}}
{{eqn | ll= \leadsto
      | l = \card S
      | r = \card t
      | c = {{Defof|Cardinal Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Set Union Equivalent to Associated Cardinal Number

Let $S$ and $T$ be sets.
Let $\card S$ denote the cardinal number of $S$.
Let $\sim$ denote set equivalence.
Then:
:$S \cup T \sim \card {S \cup T} \iff S \sim \card S \land T \sim \card T$

Proof:
=== Necessary Condition ===
Let $S \cup T \sim \card {S \cup T}$.
By definition of set equivalence, there exists a bijection:
:$f: S \cup T \to \card {S \cup T}$
Since $f$ is a bijection, it follows that:
:$S$ is equivalent to the image of $S$ under $f$.
{{explain|Link to a result proving the above.}}
This, in turn, is a subset of the ordinal $\card {S \cup T}$.
{{explain|Link to a result proving the above.}}
$\card {S \cup T}$ is an ordinal by Cardinal Number is Ordinal.
By Condition for Set Equivalent to Cardinal Number, it follows that:
:$S \sim \card S$
Similarly:
:$T \sim \card T$
{{qed|lemma}}
Theorem: Condition for Cartesian Product Equivalent to Associated Cardinal Number

Let $S$ and $T$ be nonempty sets.
Let $\card S$ denote the cardinal number of $S$.
Then:
:$S \times T \sim \card {S \times T} \iff S \sim \card S \land T \sim \card T$
where $S \times T$ denotes the cartesian product of $S$ and $T$.

Proof:
=== Necessary Condition ===
If $S \times T \sim \card {S \times T}$, then there is a mapping $f$ such that:
:$f : S \times T \to \card {S \times T}$ is a bijection.
Since $f$ is a bijection, it follows that:
:$S$ is equivalent to the image of $S \times \set x$ under $f$ where $x \in T$.
This, in turn, is a subset of the ordinal $\card {S \times T}$.
$\card {S \times T}$ is an ordinal by Cardinal Number is Ordinal.
By Condition for Set Equivalent to Cardinal Number, it follows that $S \sim \card S$.
Similarly, $T \sim \card T$.
{{qed|lemma}}
Theorem: Cardinal of Cardinal Equal to Cardinal

Let $S$ be a set such that $S$ is equivalent to its cardinal.
If the axiom of choice holds, then this condition holds for any set.
Then:
:$\card {\paren {\card S} } = \card S$
where $\card S$ denotes the cardinal number of $S$.

Proof:
By Condition for Set Equivalent to Cardinal Number:
:$S \sim \card S$
Therefore, by Equivalent Sets have Equal Cardinal Numbers:
:$\card S = \card {\paren {\card S} }$
{{qed}}
Theorem: Cardinal of Finite Ordinal

Let $n$ be a finite ordinal.
Let $\card n$ denote the cardinal number of $n$.
Then:
:$\card n = n$

Proof:
Since $n$ is an ordinal, it follows that $\card n \le n$ by {{Corollary|Cardinal Number Less than Ordinal}}.
{{MissingLinks|Predecessor of Finite Ordinal is Finite Ordinal/Element of Finite Ordinal is Finite Ordinal}}
Hence, $\card n$ is also a finite ordinal.
Since $n$ is an ordinal, it also follows that $n \sim \card n$ by Ordinal Number Equivalent to Cardinal Number.
{{link wanted|Equality of Finite Ordinals?}}
By Equality of Natural Numbers, it follows that $n = \card n$.
{{qed}}
Theorem: Finite Ordinal is equal to Natural Number

Let $n$ be an element of the minimally inductive set.
Let $x$ be an ordinal.
Then:
:$n \sim x \implies n = x$

Proof:
Let $n \ne x$.
Then either $n < x$ or $x < n$ by Ordinal Membership is Trichotomy.
{{explain|Link to the result which states that $\le$ is isomorphic to $\subseteq$ on ordinals.}}
If $x < n$, then by Subset of Finite Set is Finite both $x$ and $n$ are finite.
Therefore by No Bijection between Finite Set and Proper Subset:
:$x \not \sim n$
Suppose $n < x$.
Then $x \sim n$ implies that $x$ is finite by definition.
By No Bijection between Finite Set and Proper Subset:
:$x \not \sim n$
Therefore by Rule of Transposition:
:$n \sim x \implies n = x$
{{qed}}
Theorem: Product (Category Theory) is Unique

Let $\mathbf C$ be a metacategory.
Let $A$ and $B$ be objects of $\mathbf C$.
Let $A \times B$ and $A \times' B$ both be products of $A$ and $B$.
Then there is a unique isomorphism $u: A \times B \to A \times' B$.
That is, products are unique up to unique isomorphism.
{{expand|cover extended theorem (for general def)}}

Proof:
Denote the implicit projections of the two products by:
<nowiki>
$\begin{xy}\xymatrix@C=2em@L+4mu{
&
 A \times B
  \ar@/_/[ddl]_*{\textrm{pr}_1}
  \ar@/^/[ddr]^*{\textrm{pr}_2}
\\ &
 A \times' B
  \ar[dl]^*{\textrm{pr}'_1}
  \ar[dr]_*{\textrm{pr}'_2}
\\
 A
& &
 B
}\end{xy}$
</nowiki>
By the universal mapping property of $A \times' B$, there is a unique $u: A \times B \to A \times' B$ fitting the dashed arrow in:
<nowiki>
$\begin{xy}\xymatrix@C=2em@L+4mu{
&
 A \times B
  \ar@/_/[ddl]_*{\textrm{pr}_1}
  \ar@/^/[ddr]^*{\textrm{pr}_2}
  \ar@{-->}[d]
\\ &
 A \times' B
  \ar[dl]^*{\textrm{pr}'_1}
  \ar[dr]_*{\textrm{pr}'_2}
\\
 A
& &
 B
}\end{xy}$
</nowiki>
By the universal mapping property of $A \times B$, there is a further unique $v: A \times' B \to A \times B$ fitting the dashed arrow in:
<nowiki>
$\begin{xy}\xymatrix@C=2em@L+4mu{
&
 A \times B
  \ar@/_/[ddl]_*{\textrm{pr}_1}
  \ar@/^/[ddr]^*{\textrm{pr}_2}
  \ar[d]^*{u}
\\ &
 A \times' B
  \ar[dl]^*{\textrm{pr}'_1}
  \ar[dr]_*{\textrm{pr}'_2}
  \ar@{-->}[d]
\\
 A
&
 A \times B
  \ar[l]^*{\textrm{pr}_1}
  \ar[r]_*{\textrm{pr}_2}
&
 B
}\end{xy}$
</nowiki>
We can now form the following diagram:
<nowiki>
$\begin{xy}\xymatrix@C=2em@R=3em@L+4mu{
 &
A \times B
  \ar[dl]_*{\textrm{pr}_1}
  \ar[dr]^*{\textrm{pr}_2}
  \ar@{-->}[d]
\\
 A
&
 A \times B
  \ar[l]^*{\textrm{pr}_1}
  \ar[r]_*{\textrm{pr}_2}
&
 B
}\end{xy}$
</nowiki>
where we see both the identity morphism $\operatorname{id}_{A \times B}$ and $v \circ u$ fit the dashed arrow.
The universal mapping property of $A \times B$ however states that there is a unique fitting morphism.
Hence $v \circ u = \operatorname{id}_{A \times B}$.
That $u \circ v = \operatorname{id}_{A \times' B}$ follows, {{Mutatis}}, by interchanging $A \times B$ and $A \times' B$.
Hence there is a unique isomorphism $u: A \times B \to A \times' B$, as desired.
{{qed}}
Theorem: Ordinal Subset is Well-Ordered

Let $S$ be a class.
{{explain|Is the $S$ really a class? All links below are for a set.}}
Let every element of $S$ be an ordinal.
Then $\struct {S, \in}$ is a strict well-ordering.

Proof:
{{improve|wrong use of links}}
Let $\On$ denote the class of all ordinals.
By definition of subset, $S \subseteq \On$.
But by Class of All Ordinals is Ordinal $\On$ is an ordinal.
Therefore $\On$ is well-ordered by $\in$.
This means that $S$ is also well-ordered by $\in$.
{{qed}}
Category:Ordinals
t5z8hn3ab8s3knfjl0g0yna92rhrjkc
Theorem: Subset implies Cardinal Inequality

Let $S$ and $T$ be sets such that $S \subseteq T$.
Furthermore, let:
:$T \sim \card T$
where $\card T$ denotes the cardinality of $T$.
Then:
:$\card S \le \card T$

Proof:
For the proof:
:the ordering relation $\le$ for ordinals
and
:the subset relation $\subseteq$
shall be used interchangeably.
Let $f: T \to \card T$ be a bijection.
It follows that $f \restriction_S : S \to \card T$ is an injection.
The image of $S$ under $f$ is a subset of $\card T$ and thus is a subset of an ordinal.
By Unique Isomorphism between Ordinal Subset and Unique Ordinal, there is a unique mapping $\phi$ and a unique ordinal $x$ such that $\phi: x \to f \sqbrk S$ is an order isomorphism.
It follows that $S \sim x$ by the definition of order isomorphism.
Furthermore, $\phi$ is a strictly increasing mapping from ordinals to ordinals.
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \le
      | r = \map \phi y
      | c = Strictly Increasing Ordinal Mapping Inequality
}}
{{eqn | o = \in
      | r = f \sqbrk  S
      | c = Definition of $\phi$
}}
{{eqn | o = \subseteq
      | r = \card T
      | c = Image Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \card T
      | c = Cardinal Number is Ordinal
}}
{{end-eqn}}
Therefore, $y \in x \implies y \in \card T$ and $x \le \card T$ by the definition of subset.
But $\card S \le x$ by Cardinal Number Less than Ordinal.
So $\card S \le \card T$ by the fact that Subset Relation is Transitive.
{{qed}}
Theorem: Subset of Ordinal implies Cardinal Inequality

Let $S$ be a set.
Let $x$ be an ordinal such that $S \subseteq x$.
Then:
:$\card S \le \card x$
where $\card S$ denotes the cardinality of $S$.

Proof:
Since $x$ is an ordinal, it follows that $x \sim \card x$ by Ordinal Number Equivalent to Cardinal Number.
This satisfies the hypothesis for Subset implies Cardinal Inequality.
Therefore:
:$\card S \le \card x$
{{qed}}
Theorem: Set Less than Cardinal Product

Let $S$ and $T$ be sets.
Let $T$ be nonempty.
Suppose that $S \times T \sim \card {S \times T}$.
Then:
:$\card S \le \card {S \times T}$

Proof:
Let $y \in T$.
Define the mapping $f : S \to S \times T$ as follows:
:$\map f x = \tuple {x, y}$
If $\map f {x_1} = \map f {x_2}$, then $\tuple {x_1, y} = \tuple {x_2, y}$ by the definition of $f$.
It follows that $x_1 = x_2$ by Equality of Ordered Pairs.
Thus, $f: S \to S \times T$ is an injection.
By Injection implies Cardinal Inequality, it follows that $\card S \le \card {S \times T}$
{{qed}}
Theorem: Injection implies Cardinal Inequality

Let $S$ and $T$ be sets.
Let $f: S \to T$ be an injection.
Let $\card T$ denote the cardinal number of $T$.
Let:
:$T \sim \card T$
where $\sim$ denotes set equivalence
Then:
:$\card S \le \card T$

Proof:
Let $f \sqbrk S$ denote the image of $S$ under $f$.
{{begin-eqn}}
{{eqn | l = S
      | o = \sim
      | r = f \sqbrk S
      | c = Set is Equivalent to Image under Injection
}}
{{eqn | o = \subseteq
      | r = T
      | c = Image Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = \card S
      | r = \card {f \sqbrk S}
      | c = Equivalent Sets have Equal Cardinal Numbers
}}
{{eqn | o = \le
      | r = \card T
      | c = Subset implies Cardinal Inequality
}}
{{end-eqn}}
{{qed}}
Category:Cardinals
tua6h54zbpnzh0nqtbpd8wt33rgftl8
Theorem: Set is Equivalent to Image under Injection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be an injection.
Then the image of $S$ under $f$ is equivalent to $S$.

Proof:
{{ProofWanted}}
Category:Set Theory
Category:Injections
n03hbds288gm7nqe1bo4sqrh78r8y1g
Theorem: Cardinality of Image of Mapping not greater than Cardinality of Domain

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\card S$ denote the cardinal number of $S$.
Then:
:$\card {\Img f} \le \card S$

Proof:
By Restriction of Mapping to Image is Surjection, the mapping:
:$f: S \to \Img f$
is a surjection.
Let $h$ be a mapping such that:
:$h: \card S \to S$
is a bijection.
By Composite of Surjections is Surjection:
:$f \circ h: \card S \to \Img f$
is a surjection.
Construct a set $R$ such that:
:$R = \set {x \in \card S: \forall y \in x: \map f {\map h x} \ne \map f {\map h y} }$
It follows that:
:$R \subseteq \card S$
By Subset of Ordinal implies Cardinal Inequality:
:$\card R \le \card S$
Suppose:
:$x \in R$
:$y \in R$
:$\map f {\map h x} = \map f {\map h y}$
Then, $x$ and $y$ are ordinals and by Ordinal Membership is Trichotomy:
:$x < y \lor x = y \lor y < x$
If $x < y$, then:
:$\map f {\map h x} \ne \map f {\map h y}$ by the definition of $R$.
Similarly, $y < x$ implies that:
:$\map f {\map h x} \ne \map f {\map h y}$
Therefore, $x = y$.
It follows that the restriction $f \circ h \restriction_R : R \to \Img f$ is an injection.
{{qed|lemma}}
Finally, by the definition of surjection, for all $x \in \Img f$, there is some $y \in \card S$ such that:
:$\map f {\map h y} = x$
But since this is true for some $y$, the set:
:$\set {\map y \in \card S: \map f {\map h y} = x}$
has a minimal element.
For this minimal element $y$, it follows that:
:$\forall z \in y: \map f {\map h z} \ne \map f {\map h y}$
since if it were equal, this would contradict the fact that $y$ is a $\in$-minimal element.
It follows that the restriction $f \circ h \restriction_R : R \to \Img f$ is a bijection.
By the definition of set equivalence, $R \sim \Img f$.
So:
{{begin-eqn}}
{{eqn | l = \Img f
      | r = \card R
      | c = Equivalent Sets have Equal Cardinal Numbers
}}
{{eqn | o = \le
      | r = \card S
      | c = Subset implies Cardinal Inequality
}}
{{end-eqn}}
{{qed}}
Theorem: Injection iff Cardinal Inequality

Let $\card T$ denote the cardinal number of $T$.
Let $S$ and $T$ be sets such that $S \sim \card S$ and $T \sim \card T$.
Then:
:$\card S \le \card T $ {{iff}} there exists an injection $f: S \to T$.

Proof:
=== Necessary Condition ===
Suppose that $\card S \le \card T$.
Let $g : S \to \card S$ be a bijection and $h: \card T \to T$ be a bijection.
It follows that $g: S \to \card T$ is an injection by the fact that $\card T \le \card S$.
Then from Composite of Injections is Injection, $h \circ g: S \to T$ is an injection.
{{qed|lemma}}
Theorem: Surjection iff Cardinal Inequality

Let $S$ and $T$ be sets.
Let $S$ be non-empty.
Then:
:$0 < \card T \le \card S$
{{iff}}:
:there exists a surjection $f: S \to T$
where $\card S$ denotes the cardinality of $S$.

Proof:
=== Necessary Condition ===
Suppose $f: S \to T$ is a surjection.
Then $\Img f = T$ by definition.
From Cardinality of Image of Mapping not greater than Cardinality of Domain:
:$\card T \le \card S$
Furthermore, if $S$ is non-empty, then $\map f x \in T$ for some $x \in S$.
Thus, $T$ is non-empty and $0 < \card T$ by Cardinality of Empty Set.
{{qed|lemma}}
Theorem: Right Identity while exists Right Inverse for All is Identity

Let $\struct  {S, \circ}$ be a semigroup with a right identity $e_R$ such that:
:$\forall x \in S: \exists x_R: x \circ x_R = e_R$
That is, every element of $S$ has a right inverse with respect to the right identity.
Then $e_R$ is also a left identity, that is, is an identity.

Proof:
Let $x \in S$ be any element of $S$.
From Right Inverse for All is Left Inverse we have that $x_R \circ x = e_R$.
Then:
{{begin-eqn}}
{{eqn | l = e_R \circ x
      | r = \paren {x \circ x_R} \circ x
      | c = {{Defof|Right Inverse Element}}
}}
{{eqn | r = x \circ \paren {x_R \circ x}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x \circ e_R
      | c = Right Inverse for All is Left Inverse
}}
{{eqn | r = x
      | c = {{Defof|Right Identity}}
}}
{{end-eqn}}
So $e_R$ behaves as a left identity as well as a right identity.
That is, by definition, $e_R$ is an identity element.
{{qed}}