avewright/proofwiki-math huggingface dataset:
Theorem: Cantor-Bernstein-Schröder Theorem/Proof 6

Let $A$ and $B$ be sets.
Let $f: A \to B$ and $g: B \to A$ be injections.
Then there is a bijection $h: A \to B$; so that $A$ and $B$ are equivalent.
Furthermore:
:For all $x \in A$ and $y \in B$, if $y = \map h x$ then either $y = \map f x$ or $x = \map g y$.

Proof:
Let $\powerset A$ be the power set of $A$.
Define a mapping $E: \powerset A \to \powerset A$ thus:
:$\map E S = A \setminus g \sqbrk {B \setminus f \sqbrk S}$
=== $E$ is increasing ===
Let $S, T \in \powerset A$ such that $S \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = f \sqbrk S
      | o = \subseteq
      | r = f \sqbrk T
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = B \setminus f \sqbrk T
      | o = \subseteq
      | r = B \setminus f \sqbrk S
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{eqn | ll= \leadsto
      | l = g \sqbrk {B \setminus f \sqbrk T}
      | o = \subseteq
      | r = g \sqbrk {B \setminus f \sqbrk S}
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = A \setminus g \sqbrk {B \setminus f \sqbrk S}
      | o = \subseteq
      | r = A \setminus g \sqbrk {B \setminus f \sqbrk T}
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{end-eqn}}
That is, $\map E S \subseteq \map E T$.
{{qed|lemma}}
By the Knaster-Tarski Lemma, $E$ has a fixed point $X$.
By the definition of fixed point:
:$\map E X = X$
Thus by the definition of $E$:
:$A \setminus g \sqbrk {B \setminus f \sqbrk X} = X$
Therefore:
:$(1): \quad A \setminus \paren {A \setminus g \sqbrk {B \setminus f \sqbrk X} } = A \setminus X$
Since $g$ is a mapping into $A$:
:$g \sqbrk {B \setminus f \sqbrk X} \subseteq A$
Thus by Relative Complement of Relative Complement:
:$A \setminus \paren {A \setminus g \sqbrk {B \setminus f \sqbrk X} } = g \sqbrk {B \setminus f \sqbrk X}$
Thus by $(1)$:
:$g \sqbrk {B \setminus f \sqbrk X} = A \setminus X$
Let $f' = f \restriction_{X \times f \sqbrk X}$ be the restriction of $f$ to $X \times f \sqbrk X$.
Similarly, let $g' = g \restriction_{\paren {B \setminus f \sqbrk X} \times \paren {A \setminus X} } = g \restriction_{\paren {B \setminus f \sqbrk X} \times g \sqbrk {B \setminus f \sqbrk X} }$.
By Injection to Image is Bijection, $f'$ and $g'$ are both bijections.
Define a relation $h: A \to B$ by $h = f' \cup {g'}^{-1}$.
We will show that $h$ is a bijection from $A$ onto $B$.
The domain of $f'$ is $X$, which is disjoint from the codomain, $A \setminus X$, of $g'$.
The domain of $g'$ is $B \setminus f \sqbrk X$, which is disjoint from the codomain, $f \sqbrk X$, of $f'$.
Let $h = f' \cup {g'}^{-1}$.
By {{Corollary|Union of Bijections with Disjoint Domains and Codomains is Bijection}}:
: $h$ is a bijection from $X \cup \paren {A \setminus X}$ onto $f \sqbrk X \cup \paren {B \setminus f \sqbrk X}$.
By Union with Relative Complement, $h$ is a bijection from $A$ onto $B$.
Since $f' \subseteq f$ and $g' \subseteq g$, each element of $h$ is an element of $f$ or of $g^{-1}$.
That is, if $y = \map h x$ then either $y = \map f x$ or $x = \map g y$.
{{Qed}}
Theorem: Ring of Polynomial Forms over Integral Domain is Integral Domain

Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$.
Let $\struct {D \sqbrk X, \oplus, \odot}$ be the ring of polynomial forms over $D$ in the indeterminate $X$.
Then $\struct {D \sqbrk X, \oplus, \odot}$ is an integral domain.

Proof:
By definition an integral domain is a commutative ring with unity. 
From Ring of Polynomial Forms is Commutative Ring with Unity it follows that $\struct {D \sqbrk X, +, \circ}$ is a commutative ring with unity.
Suppose $f, g \in D \sqbrk X$ such that neither $f$ nor $g$ are the null polynomial.
Let $\map \deg f = n$ and $\map \deg g = m$.
From Degree of Product of Polynomials over Integral Domain the degree of $f \odot g$ is $n + m$.
Thus by definition $f \odot g$ is not the null polynomial of $D \sqbrk X$.
Thus neither $f$ nor $g$ is a proper zero divisor of $D \sqbrk X$.
This holds for any two arbitrary non-null polynomials elements of $D \sqbrk X$.
Hence $\struct {D \sqbrk X, \oplus, \odot}$ is a commutative ring with unity with no proper zero divisors.
That is, $\struct {D \sqbrk X, \oplus, \odot}$ is an integral domain.
{{qed}}
Theorem: Union of One-to-Many Relations with Disjoint Images is One-to-Many

Let $S_1, S_2, T_1, T_2$ be sets or classes.
Let $\RR_1$ be a one-to-many relation on $S_1 \times T_1$.
Let $\RR_2$ be a one-to-many relation on $S_2 \times T_2$.
Suppose that the images of $\RR_1$ and $\RR_2$ are disjoint.
Then $\RR_1 \cup \RR_2$ is a one-to-many relation on $\paren {S_1 \cup S_2} \times \paren {T_1 \cup T_2}$.

Proof:
Let $\QQ = \RR_1 \cup \RR_2$.
Then $\QQ \subseteq \paren {S_1 \times T_1} \cup \paren {S_2 \times T_2} \subseteq \paren {S_1 \cup S_2} \times \paren {T_1 \cup T_2}$.
Thus $\QQ$ is a relation on $\paren {S_1 \cup S_2} \times \paren {T_1 \cup T_2}$.
Let $T'_1$ and $T'_2$ be the images of $\RR_1$ and $\RR_2$, respectively.
Let $\tuple {x_1, y}, \tuple {x_2, y} \in \QQ$.
Then $y \in T'_1$ or $y \in T'_2$.
If $y \in T'_1$ then $y \notin T'_2$, so neither $\tuple {x_1, y}$ nor $\tuple {x_2, y}$ is in $\RR_2$, so these pairs are both in $\RR_1$.
As $\RR_1$ is one-to-many, $x_1 = x_2$.
A similar argument leads to the same result for $y \in T'_2$.
As this holds for all such $x_1, x_2, y$: $\QQ$ is a one-to-many relation.
{{qed}}
Category:Relation Theory
mtfp6uex1k785blrxeto0eqv61i8e3r
Theorem: Union of Many-to-One Relations with Disjoint Domains is Many-to-One

Let $S_1, S_2, T_1, T_2$ be sets or classes.
Let $\RR_1$ be a many-to-one relation on $S_1 \times T_1$.
Let $\RR_2$ be a many-to-one relation on $S_2 \times T_2$.
Suppose that the domains of $\RR_1$ and $\RR_2$ are disjoint.
Then $\RR_1 \cup \RR_2$ is a many-to-one relation on $\paren {S_1 \cup S_2} \times \paren {T_1 \cup T_2}$.

Proof:
Let $\RR = \RR_1 \cup \RR_2$.
Let $\tuple {x, y_1}, \tuple {x, y_2} \in \RR$.
By the definition of union, $\tuple {x, y_1}$ and $\tuple {x, y_2}$ are each in $\RR_1$ or $\RR_2$.
Suppose that both are in $\RR_1$.
Then since $\RR_1$ is a many-to-one relation, $y_1 = y_2$.
Suppose that $\tuple {x, y_1} \in \RR_1$ and $\tuple {x, y_2} \in \RR_2$.
Then $x$ is in the domain of $\RR_1$ and that of $\RR_2$, contradicting the premise, so this cannot occur.
The other two cases are precisely similar.
Thus in all cases $y_1 = y_2$.
As this holds for all such pairs, $\RR$ is many-to-one.
{{qed}}
Category:Relation Theory
93vaix66p8b4htn9iiddor48mxwxzmb
Theorem: Nth Root of Integer is Integer or Irrational

Let $n$ be a natural number.
Let $x$ be an integer.
If the $n$th root of $x$ is not an integer, it must be irrational.

Proof:
We prove the contrapositive: if the $n$th root of $x$ is rational, it must be an integer.
By Existence of Canonical Form of Rational Number, there exist an integer $a$ and a natural number $b$ which are coprime such that:
{{begin-eqn}}
{{eqn | l = x^{1/n}
      | r = \frac a b
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \frac {a^n} {b^n}
}}
{{end-eqn}}
Since $a$ and $b$ are coprime, $a^n$ and $b^n$ are coprime by Powers of Coprime Numbers are Coprime.
Hence $\dfrac {a^n} {b^n}$ is by definition in canonical form.
Suppose $b \ne 1$.
As the denominator of $\dfrac {a^n} {b^n}$ is not $1$, $x = \dfrac {a^n} {b^n}$ is not an integer.
This is a contradiction.
Thus $b = 1$, and thus:
:$x^{1/n} = a$
which is an integer.
{{qed}}
Theorem: Union of Bijections with Disjoint Domains and Codomains is Bijection

Let $A$, $B$, $C$, and $D$ be sets or classes.
Let $A \cap B = C \cap D = \O$.
Let $f: A \to C$ and $g: B \to D$ be bijections.
Then $f \cup g: A \cup B \to C \cup D$ is also a bijection.

Proof:
By the definition of bijection, $f$ and $g$ are many-to-one and one-to-many relations.
By Union of Many-to-One Relations with Disjoint Domains is Many-to-One and Union of One-to-Many Relations with Disjoint Images is One-to-Many:
:$f \cup g$ is many-to-one and one-to-many.
Thus to show $f \cup g$ is a bijection requires us only to demonstrate that it is both left-total and right-total.
We will show that $f \cup g$ is left-total.
Let $x \in A \cup B$.
Then $x \in A$ or $x \in B$.
If $x \in A$ then since $f$ is left-total there is a $y \in C$ such that $\tuple {x, y} \in f$.
By the definition of union, $\tuple {x, y} \in f \cup g$.
If $x \in B$ then since $g$ is left-total there is a $y \in D$ such that $\tuple {x, y} \in g$.
Then by the definition of union, $\tuple {x, y} \in f \cup g$.
As this holds for all $x$, $f \cup g$ is left-total.
The proof that $f \cup g$ is right-total is similar.
Thus it has been demonstrated that:
:$f \cup g$ is many-to-one
:$f \cup g$ is one-to-many
:$f \cup g$ is left-total
:$f \cup g$ is right-total
and therefore, by definition, a bijection.
{{qed}}
Category:Bijections
Category:Set Union
Category:Union of Bijections with Disjoint Domains and Codomains is Bijection
j4b0sbgqb440x7bfv3jkp6zffcnsmfp
Theorem: Closed Interval in Complete Lattice is Complete Lattice

Let $\struct {L, \preceq}$ be a complete lattice.
Let $a, b \in L$ with $a \preceq b$.
Let $I = \closedint a b$ be the closed interval between $a$ and $b$.
{{explain|Demonstrate that for each $a, b \in L$ that $\closedint a b$ exists and is unique.}}
Then $\struct {I, \preceq}$ is also a complete lattice.

Proof:
Let $S \subseteq I$.
If $S = \O$, then it has a supremum in $I$ of $a$ and an infimum in $I$ of $b$.
Let $S \ne \O$.
Since $S \subseteq I$, $a$ is a lower bound of $S$ and $b$ is an upper bound of $S$.
Since $L$ is a complete lattice, $S$ has an infimum, $p$, and a supremum, $q$, in $L$.
Thus by the definitions of infimum and supremum:
:$a \preceq p$ and $q \preceq b$
Let $x \in S$.
Since an infimum is a lower bound:
:$p \preceq x$
Since a supremum is an upper bound:
:$x \preceq q$
Thus $a \preceq p \preceq x \preceq q \preceq b$.
Since $\preceq$ is an ordering, it is transitive, so by Transitive Chaining:
:$a \preceq p \preceq b$ and $a \preceq q \preceq b$.
That is, $p, q \in I$.
Thus $p$ and $q$ are the infimum and supremum of $S$ in $I$.
As every subset of $I$ has a supremum and infimum in $I$, $I$ is a complete lattice.
{{qed}}
Theorem: Dedekind-Complete Bounded Ordered Set is Complete Lattice

Let $\struct {L, \preceq}$ be an ordered set.
Let $L$ have a lower bound $\bot$ and an upper bound $\top$.
Let $\struct {L, \preceq}$ be Dedekind-complete.
Then $\struct {L, \preceq}$ is a complete lattice.

Proof:
Let $S \subseteq L$.
If $S = \O$, then $S$ has a supremum of $\bot$ and an infimum of $\top$.
Let $S \ne \O$.
$S$ is bounded above by $\top$.
As $\struct {L, \preceq}$ is Dedekind complete, $S$ has a supremum.
$S$ is bounded below by $\bot$.
By Dedekind Completeness is Self-Dual, $S$ has an infimum.
Thus every subset of $L$ has a supremum and an infimum.
So, by definition, $\struct {L, \preceq}$ is a complete lattice.
{{qed}}
Category:Complete Lattices
i4gxl3fiak2hg73kbcmxqnm1sztdb36
Theorem: Set Difference with Subset is Superset of Set Difference

Let $A, B, S$ be sets or classes.
Suppose that $A \subseteq B$.
Then:
:$S \setminus B \subseteq S \setminus A$
where $\setminus$ represents set difference.

Proof:
Let $x \in S \setminus B$.
Then by definition of set difference:
:$x \in S$ and $x \notin B$
{{AimForCont}} $x \in A$.
Then since $A$ is a subset (or subclass) of $B$, $x \in B$, a contradiction.
Thus $x \notin A$.
Since $x \in S$ and $x \notin A$, we conclude that $x \in S \setminus A$.
As this holds for all $x \in S \setminus B$:
:$S \setminus B \subseteq S \setminus A$
{{qed}}
Category:Set Difference
cxw2oitgt5ky9ao5ke5bu1nw6l2tdvy
Theorem: Knaster-Tarski Lemma/Corollary

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a fixed point

Proof:
By the Knaster-Tarski Lemma, $f$ has a least fixed point.
Thus it has a fixed point.
{{qed}}
Category:Knaster-Tarski Lemma
5rvzccftb6yjfu5kjc2201xq80xzx0b
Theorem: Knaster-Tarski Lemma/Corollary

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a fixed point

Proof:
By the Knaster-Tarski Lemma: Power Set, $f$ has a least fixed point.
Thus it has a fixed point.
{{qed}}
Theorem: Knaster-Tarski Lemma/Corollary

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a fixed point

Proof:
Let $P = \set {x \in \powerset S: x \subseteq \map f x}$.
Let $\ds \bigcup P$ be the union of $P$.
Let $x \in P$.
Then by Set is Subset of Union: General Result:
:$\ds x \subseteq \bigcup P$
Since $f$ is increasing, $\map f x \subseteq \map f {\bigcup P}$.
By definition of $P$, $x \subseteq \map f x$.
Thus $\ds x \subseteq \map f {\bigcup P}$ by Subset Relation is Transitive:
As this holds for all $x \in P$,  by Union is Smallest Superset: General Result:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Now since $f$ is increasing:
:$\ds \map f {\bigcup P} \subseteq \map f {\map f {\bigcup P} }$
Thus $\ds \map f {\bigcup P} \in P$ by definition of $P$.
Therefore by Set is Subset of Union: General Result:
:$\ds \map f {\bigcup P} \subseteq \bigcup P$
We have that:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Thus by definition of set equality:
:$\ds \map f {\bigcup P} = \bigcup P$
Thus $\ds \bigcup P$ is a fixed point of $f$.
{{qed}}
Theorem: Knaster-Tarski Lemma/Corollary/Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $f: \powerset S \to \powerset S$ be a $\subseteq$-increasing mapping.
That is, suppose that for all $T, U \in \powerset S$:
:$T \subseteq U \implies \map f T \subseteq \map f U$
Then $f$ has a fixed point.

Proof:
By the Knaster-Tarski Lemma: Power Set, $f$ has a least fixed point.
Thus it has a fixed point.
{{qed}}
Theorem: Knaster-Tarski Lemma/Corollary/Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $f: \powerset S \to \powerset S$ be a $\subseteq$-increasing mapping.
That is, suppose that for all $T, U \in \powerset S$:
:$T \subseteq U \implies \map f T \subseteq \map f U$
Then $f$ has a fixed point.

Proof:
Let $P = \set {x \in \powerset S: x \subseteq \map f x}$.
Let $\ds \bigcup P$ be the union of $P$.
Let $x \in P$.
Then by Set is Subset of Union: General Result:
:$\ds x \subseteq \bigcup P$
Since $f$ is increasing, $\map f x \subseteq \map f {\bigcup P}$.
By definition of $P$, $x \subseteq \map f x$.
Thus $\ds x \subseteq \map f {\bigcup P}$ by Subset Relation is Transitive:
As this holds for all $x \in P$,  by Union is Smallest Superset: General Result:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Now since $f$ is increasing:
:$\ds \map f {\bigcup P} \subseteq \map f {\map f {\bigcup P} }$
Thus $\ds \map f {\bigcup P} \in P$ by definition of $P$.
Therefore by Set is Subset of Union: General Result:
:$\ds \map f {\bigcup P} \subseteq \bigcup P$
We have that:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Thus by definition of set equality:
:$\ds \map f {\bigcup P} = \bigcup P$
Thus $\ds \bigcup P$ is a fixed point of $f$.
{{qed}}
Theorem: Natural Number has Same Prime Factors as Integer Power

Let $x$ be a natural number such that $x > 1$.
Let $n \ge 1$ be a (strictly) positive integer.
The $n$th power of $x$ has the same prime factors as $x$.

Proof:
Let $p$ be a prime number such that $p$ divides $x^n$.
This is possible because $x > 1$, so $x^n > 1$, hence $x^n$ has prime divisors due to Fundamental Theorem of Arithmetic.
To prove the statement, we need to show $p$ divides $x$.
We will prove this statement by the Principle of Mathematical Induction on $n$.
=== Basis of the Induction ===
We have $n = 1$
Clearly, since $p$ divides $x^1 = x$, then $p$ divides $x$.
{{qed |lemma}}
=== Inductive Step ===
Suppose that for a given $n$, if $p$ divides $x^n$ then $p$ divides $x$. 
Then, if $p$ divides $x^{n + 1}$, by Euclid's Lemma for Prime Divisors, either $p$ divides $x^n$ or $p$ divides $x$.
If $p$ divides $x^n$, we get from the induction hypothesis that $p$ divides $x$.
The other case trivially leads to our conclusion.
{{qed|lemma}}
Hence the result, by Principle of Mathematical Induction.
{{qed|lemma}}
Conversely, let $p$ a prime number such that it divides $x$. 
Then $p$ divides $x \times x^{n - 1} = x^n$, as required.
{{qed}}
Theorem: Alternative Definition of Ordinal in Well-Founded Theory

A set $S$ is an ordinal {{iff}} $S$ is transitive and $\forall x, y \in S: \paren {x \in y \lor x = y \lor y \in x}$.

Proof:
=== Forward Implication ===
Let $S$ be an ordinal.
By Alternative Definition of Ordinal, $S$ is transitive and strictly well-ordered by the epsilon relation.
By Strict Well-Ordering is Strict Total Ordering, $S$ is strictly totally ordered by $\in$.
Thus:
:$\forall x, y \in S: \paren {x \in y \lor x = y \lor y \in x}$
{{qed|lemma}}
Theorem: Strictly Well-Founded Relation is Antireflexive/Corollary

Let $\struct {S, \preceq}$ be an ordered set.
Suppose that $S$ is non-empty.
Then $\preceq$ is not a strictly well-founded relation.

Proof:
Since $S$ is non-empty, it has an element $x$.
By the definition of ordering, $\preceq$ is a reflexive relation.
Thus $x \preceq x$.
By Strictly Well-Founded Relation is Antireflexive, $\preceq$ is not a strictly well-founded relation.
{{qed}}
Category:Well-Founded Relations
jonolnxmr636hgrl1f6j1fcs4elutvy
Theorem: Reflexive Reduction of Well-Founded Relation is Strictly Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation on $S$.
Let $\RR^{\ne}$ be the reflexive reduction of $\RR$.
Then $\RR^{\ne}$ is a strictly well-founded relation.

Proof:
Let $T$ be a non-empty subset of $S$.
Since $\RR$ is a well-founded relation, $T$ has a minimal element with respect to the relation $\RR$.
That is, there is an element $m \in T$ such that $\forall x \in T: \paren {\tuple {x, m} \notin \RR} \lor \paren {x = m}$.
Let $x \in T$.
Then $\tuple {x, m} \notin \RR$ or $x = m$.
By the definition of reflexive reduction, $\RR^{\ne}$ is a subset of $\RR$.
Thus:
:if $\tuple {x, m} \notin \RR$, it follows that $\tuple {x, m} \notin \RR^{\ne}$.
:if $x = m$ then by Reflexive Reduction is Antireflexive, $\tuple {x, m} \notin \RR^{\ne}$.
As $x$ is arbitrary, this holds for all $x \in T$.
Thus $m$ is a strictly minimal element under $\RR^{\ne}$ in $T$.
As $T$ is arbitrary, this condition holds for all non-empty subsets of $S$.
That is, every non-empty subset of $S$ has a strictly minimal element under $\RR^{\ne}$.
Hence, by definition, $\RR^{\ne}$ is a strictly well-founded relation on $S$.
{{qed}}
Category:Reflexive Reductions
Category:Well-Founded Relations
8o239xep8bb50vupw7p9ww25oqrwo01
Theorem: Epsilon Relation is Proper

Let $\mathbb U$ be the universal class.
Let $\Epsilon$ be the epsilon relation.
Then $\struct {\mathbb U, \Epsilon}$ is a proper relational structure.

Proof:
{{NotZFC}}
Let $x \in \mathbb U$.
Then by the Axiom of Extension:
:$x = \map {\Epsilon^{-1} } x$
where $\map {\Epsilon^{-1} } x$ denotes the preimage of $x$ under $\Epsilon$.
Since $x$ is a set, $\map {\prec^{-1} } x = x$ is a set.
As this holds for all $x \in \mathbb U$, $\struct {\mathbb U, \Epsilon}$ is a proper relational structure.
{{qed}}
Category:Class Theory
dvipnnoo0n36c8amybyy6zksla9l7c7
Theorem: Relationship between Transitive Closure Definitions

Let $x$ be a set.
Let $a$ be the smallest set such that $x \in a$ and $a$ is transitive.
Let $b$ be the smallest set such that $x \subseteq b$ and $b$ is transitive.
Then $a = b \cup \set x$.

Proof:
We have that:
:$x \in a$
and $a$ is transitive.
So:
:$x \subseteq a$
Thus by the definition of $b$ and of smallest set:
:$b \subseteq a$
Since we also have $x \in a$:
:$b \cup \set x \subseteq a$
$x \in \set x$, so:
:$x \in b \cup \set x$
$b \cup \set x$ is transitive:
If $p \in b$ then:
:$p \subseteq b \subseteq b \cup \set x$.
If $p \in \set x$ then:
:$p = x$
So by the definition of $b$:
:$p \subseteq b \subseteq b \cup \set x$
Thus by the definition of $a$:
:$a \subseteq b \cup \set x$
Thus the theorem holds by definition of set equality.
{{qed}}
Category:Set Theory
l7ziwup2v5r1puow7hgnuvd76gft23u
Theorem: Ordinal is not Element of Itself

Let $x$ be an ordinal.
Then:
:$x \notin x$

Proof:
By Successor Set of Ordinal is Ordinal, the successor of $x$ is an ordinal.
That is, $x^+ = x \cup \set x$ is an ordinal.
By Set is Element of Successor, $x \in x^+$.
Because $x^+$ is an ordinal, it is strictly well-ordered by the epsilon restriction $\Epsilon {\restriction_{x^+} }$.
Because a strict ordering is antireflexive and $x \in x^+$, we conclude that $x \notin x$.
{{qed}}
Theorem: Ordinal is not Element of Itself

Let $x$ be an ordinal.
Then:
:$x \notin x$

Proof:
This result follows immediately from Set is Not Element of Itself.
{{qed}}
Theorem: Ordinal is not Element of Itself

Let $x$ be an ordinal.
Then:
:$x \notin x$

Proof:
Let $\On$ denote the class of all ordinals.
From Class of All Ordinals is Minimally Superinductive over Successor Mapping, $\On$ is superinductive.
Hence we can use the Principle of Superinduction.
By Zero is Smallest Ordinal, $0$ is the smallest element of $\On$.
We identify the natural number $0$ via the von Neumann construction of the natural numbers as:
:$0 := \O$
From Empty Set is Ordinary:
:$\O \notin \O$
and so:
:$0 \notin 0$
{{qed|lemma}}
Let $x$ be an ordinal for which it has been established that:
:$x \notin x$
Then by Successor Set of Ordinary Transitive Set is Ordinary:
:$x^+ \notin x^+$
{{qed|lemma}}
It remains to be shown that if $C$ is a chain of ordinals all of which are ordinary, then $\bigcup C$ is ordinary.
Let $C$ be a chain of ordinals.
From Union of Set of Ordinals is Ordinal, $\bigcup C$ is itself an ordinal.
Let $\alpha = \bigcup C$.
{{AimForCont}} $\bigcup C$ is not ordinary.
That is, suppose that $\alpha \in \alpha$.
Then:
:$\alpha \in \bigcup C$
Hence for some $\beta \in C$:
:$\alpha \in \beta$
But:
:$\beta \in C$
and so:
:$\beta \subseteq \bigcup C$
That is:
:$\beta \subseteq \alpha$
Because $\alpha \in \beta$ and Ordinal is Transitive:
:$\alpha \subseteq \beta$
Hence by definition of set equality:
:$\alpha = \beta$
That is:
:$\beta \in \beta$
Thus some element of $C$, that is, $\beta$, is an element of itself.
That is, not all elements of $C$ are ordinary.
This contradicts our assertion that all elements of $C$ are ordinary.
Hence by Proof by Contradiction we have that if $C$ is a chain of ordinals all of which are ordinary, then $\bigcup C$ is ordinary:
:$\bigcup C \notin \bigcup C$
{{qed|lemma}}
The result then follows by the Principle of Superinduction.
{{qed}}
Theorem: Ordinal is not Element of Itself

Let $x$ be an ordinal.
Then:
:$x \notin x$

Proof:
{{AimForCont}} $x \in x$.
From Equality is Reflexive, $x = x$.
From Ordinal Membership is Trichotomy, either $x = x$ or $x \in x$.
It follows from this contradiction that $x \notin x$.
{{qed}}
Theorem: Set is Element of Successor

Let $x$ be a set.
Let $x^+$ be the successor of $x$.
Then $x \in x^+$.

Proof:
By the definition of successor set:
: $x^+ = x \cup \{x\}$.
By the definition of singleton, $x \in \{x\}$.
Thus by the definition of union, $x \in x^+$.
{{qed}}
Category:Ordinals
7sif0tawwnckd2ghx1u58z7u5b04ugc