avewright/proofwiki-math huggingface dataset:
Theorem: Power Set of Natural Numbers has Cardinality of Continuum

Let $\N$ denote the set of natural numbers.
Let $\powerset \N$ denote the power set of $\N$.
Let $\card {\powerset \N}$ denote the cardinality of $\powerset \N$.
Let $\mathfrak c = \card \R$ denote the cardinality of the continuum.
Then:
:$\mathfrak c = \card {\powerset \N}$

Proof:
By Reals are Isomorphic to Dedekind Cuts there exists bijection:
:$f: \R \to \mathscr D$
where:
:$\mathscr D$ denotes the set of all Dedekind cuts of $\struct {\Q, \le}$.
Dedekind's cuts are subsets of $\Q$.
Therefore by definition of power set:
:$\mathscr D \subseteq \powerset \Q$
By Subset implies Cardinal Inequality:
:$\card {\mathscr D} \le \card {\powerset \Q}$
By Rational Numbers are Countably Infinite:
:$\Q$ is countably infinite.
Then by definition of countably infinite there exists a bijection:
:$g: \Q \to \N$
By definition of set equivalence:
:$\Q \sim \N$
Hence by definition of cardinality:
:$\card \Q = \card \N$
Then by Cardinality of Power Set is Invariant:
:$\card {\powerset \Q} = \card {\powerset \N}$
By definition of set equivalence:
:$\R \sim \mathscr D$
Hence by definition of cardinality:
:$\card \R = \card {\mathscr D}$
Thus:
:$\mathfrak c \le \card {\powerset \N}$
Define a mapping $h: \map {\operatorname {Fin} } \N \times \powerset \N \to \R^+$:
:$\ds \forall F \in \map {\operatorname {Fin} } \N, A \in \powerset \N: \map h {F, A} = \sum_{i \mathop \in F} 2^i + \sum_{i \mathop \in A} \paren {\frac 1 2}^i$
where $\map {\operatorname {Fin} } \N$ denotes the set of all finite subsets of $\N$.
A pair $\tuple {F, A}$ corresponds to binary denotation of a real number $\map h {F, A}$.
It means that $h$ is a surjection.
By Surjection iff Cardinal Inequality:
:$\card {\map {\operatorname {Fin} } \N \times \powerset \N} \le \card {\R^+}$
By definition of subset:
:$\map {\operatorname {Fin} } \N \subseteq \powerset \N$
Then by Subset implies Cardinal Inequality:
:$\card {\map {\operatorname {Fin} } \N} \le \card {\powerset \N}$
{{begin-eqn}}
{{eqn | l = \card {\map {\operatorname {Fin} } \N \times \powerset \N}
      | r = \max \set {\card {\map {\operatorname {Fin} } \N}, \card {\powerset \N} }
      | c = Cardinal Product Equal to Maximum
}}
{{eqn | r = \card {\powerset \N}
}}
{{end-eqn}}
Because $\R^+ \subseteq \R$, we have by Subset implies Cardinal Inequality:
:$\card {\R^+} \le \card \R$
Thus:
:$\card {\powerset \N} \le \mathfrak c$
Hence the result:
:$\mathfrak c = \card {\powerset \N}$
{{qed}}
Theorem: Empty Set can be Derived from Axiom of Abstraction

The '''empty set''' can be formed by application of the {{axiom-link|Abstraction}}.
Hence the '''empty set''' can be derived as a valid object in Frege set theory.

Proof:
Let $P$ be the property defined as:
:$\forall x: \map P x := \neg \paren {x = x}$
Hence, using the {{axiom-link|Abstraction}}, we form the set:
:$\O := \set {x: \neg \paren {x = x} }$
where the property ${\map P x}$ is:
:$\neg \paren {x = x}$
Since we have that:
:$\forall x: x = x$
it is seen that $\O$ as defined here has no elements.
By definition of Frege set theory, given any property $P$, there exists a unique set which consists of all and only those objects which have property $P$:
:$\set {x: \map P x}$
Therefore, there exists a unique set
:$\O := \set {x: \neg \paren {x = x} }$
which the property $P= \neg \paren {x = x}$, which consists of no elements.
Hence, by the definition of the '''empty set''', this set is a valid object in Frege set theory.
Hence the result by definition of the '''empty set'''.
{{qed}}
Theorem: Doubleton of Sets can be Derived using Axiom of Abstraction

Let $a$ and $b$ be sets.
By application of the {{axiom-link|Abstraction}}, the set $\set {a, b}$ can be formed.
Hence the '''doubleton''' $\set {a, b}$ can be derived as a valid object in Frege set theory.

Proof:
Let $P$ be the property defined as:
:$\forall x: \map P x := \paren {x = a \lor x = b}$
where $\lor$ is the disjunction operator.
Hence, using the {{axiom-link|Abstraction}}, we form the set:
:$\set {a, b} := \set {x: x = a \lor x = b}$
{{qed}}
Theorem: Power Set can be Derived using Axiom of Abstraction

Let $a$ be a set.
By application of the {{axiom-link|Abstraction}}, the power set $\powerset a$ can be formed.
Hence the '''power set''' $\powerset a$ can be derived as a valid object in Frege set theory.

Proof:
Let $P$ be the property defined as:
:$\forall x: \map P x := \paren {x \subseteq a}$
where $\lor$ is the disjunction operator.
Hence, using the {{axiom-link|Abstraction}}, we form the set:
:$\powerset a := \set {x: x \subseteq a}$
{{qed}}
Theorem: Set Union can be Derived using Axiom of Abstraction

Let $a$ be a set of sets.
By application of the {{axiom-link|Abstraction}}, the union $\bigcup a$ can be formed.
Hence the '''union''' $\bigcup a$ can be derived as a valid object in Frege set theory.

Proof:
Let $P$ be the property defined as:
:$\forall x: \map P x := \paren {\exists y: y \in a \land x \in y}$
where $\land$ is the conjunction operator.
That is, $\map P x$ {{iff}}:
:$x$ is an element of some set $y$, where $y$ is one of the sets that comprise the elements of $a$.
Hence, using the {{axiom-link|Abstraction}}, we form the set:
:$\bigcup a := \set {x: \exists y: y \in a \land x \in y}$
{{qed}}
Theorem: Set of Natural Numbers can be Derived using Axiom of Abstraction

Let $\N$ denote the set of natural numbers.
By application of the {{axiom-link|Abstraction}}, $\N$ can be derived as a valid object in Frege set theory.

Proof:
{{ProofWanted|Use the same construction as in ZF}}
Theorem: Frege Set Theory is Logically Inconsistent

The system of axiomatic set theory that is Frege set theory is inconsistent.

Proof:
From Russell's Paradox, the {{axiom-link|Abstraction}} leads to a contradiction.
Let $q$ be such a contradiction:
:$q = p \land \neg p$
for some statement $p$.
From the Rule of Explosion it then follows that every logical formula is a provable consequence of $q$.
Hence the result, by definition of inconsistent.
{{qed}}
Theorem: Exists Subset which is not Element

Let $S$ be a set.
Then there exists at least one subset of $S$ which is not an element of $S$.

Proof:
Let $S$ be a set.
Let $T$ be the set of all elements of $S$ which do not contain $S$ as elements.
Then by {{Corollary|Russell's Paradox}}, $T$ itself cannot be an element of $S$.
This $T$ is the required subset.
Theorem: Exists Subset which is not Element

Let $S$ be a set.
Then there exists at least one subset of $S$ which is not an element of $S$.

Proof:
Consider the power set $\powerset S$ of $S$.
From Cantor's Theorem, there is no surjection $f: S \to \powerset S$.
That is, there are more subsets of $S$ than there are elements of $S$.
So there must be at least one subset of $S$ which is not an element of $S$.
{{qed}}
Theorem: Box Topology may not be Coarsest Topology such that Projections are Continuous/Lemma

Let $\struct {X, \tau}$ be a topological space.
Let $U \in \tau$ such that $U \ne \O$ and $U \ne X$.
Let:
:$Y = \ds \prod_{n \mathop \in \N} X = X \times X \times X \times \ldots$
be the countable Cartesian product of $\family {X}_{n \mathop \in \N}$.
Let $\tau_T$ be the product topology on $Y$.
Let $\tau_b$ be the box topology on $Y$.
Let:
:$V = \ds \prod_{n \mathop \in \N} U = U \times U \times U \times \ldots$
be the countable Cartesian product of $\family {U}_{n \mathop \in \N}$.
Then:
:$V$ is an element of the box topology $\tau_b$
:$V$ is not an element of the product topology $\tau_T$

Proof:
By the definition of the box topology:
:$V \in \tau_b$
Let $W \in \tau_T$.
Theorem: P-adic Expansion Representative of P-adic Number is Unique

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a$ be a $p$-adic number, that is left coset, in $\Q_p$.
Let $\ds \sum_{i \mathop = m}^\infty d_i p^i$ and $\ds \sum_{i \mathop = k}^\infty e_i p^i$ be $p$-adic expansions that represent $a$.
Then:
:$(1) \quad m = k$
:$(2) \quad \forall i \ge m : d_i = e_i$
That is, the $p$-adic expansions $\ds \sum_{i \mathop = m}^\infty d_i p^i$ and $\ds \sum_{i \mathop = k}^\infty e_i p^i$ are identical.

Proof:
From P-adic Number times P-adic Norm is P-adic Unit there exists $n \in \Z$:
:$p^n a \in \Z^\times_p$
:$\norm a_p =  p^n$ 
where $\Z^\times_p$ is the set of $p$-adic units.
Let $l = -n$.
From P-adic Norm of P-adic Expansion is determined by First Nonzero Coefficient:
:$l = \min \set {i: i \ge m \land d_i \ne 0}$
and
:$l = \min \set {i: i \ge k \land e_i \ne 0}$
Now:
{{begin-eqn}}
{{eqn | l = m
      | o = <
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = d_m
      | o = \ne
      | r = 0
      | c = {{Defof|P-adic Expansion|$p$-adic Expansion}}
}}
{{eqn | ll= \leadsto
      | l = m
      | r = l
      | c = Definition of $l$
}}
{{eqn | ll= \leadsto
      | l = l
      | o = <
      | r = 0
}}
{{end-eqn}}
Similarly:
:$k < 0 \leadsto k = l$
Theorem: Class is Subclass of Universal Class

Let $V$ denote the universal class.
Let $A$ be a class.
Then $A$ is a subclass of $V$.

Proof:
By definition of class, $A$ is a collection of sets.
Let $x \in A$ be a set.
By definition of universal class, $V$ contains all sets as elements.
Hence $x \in V$.
So we have that:
:$x \in A \implies x \in V$
and the result follows by definition of subclass.
{{qed}}
Theorem: Not Every Class is a Set

Let $A$ be a class.
Then it is not necessarily the case that $A$ is also a set.

Proof:
Let a set $x$ be defined as ordinary {{iff}} $x \notin x$.
Let $\map \phi x$ be the set property defined as:
:$\map \pi x := \neg \paren {x \in x}$
Then by the Axiom of Specification there exists a class, which can be denoted $A$, such that:
:$A = \set {x: \neg \paren {x \in x} }$
By the Axiom of Extension, $A$ is unique.
Thus $A$ is the class of all ordinary sets.
Hence we have:
:$x \in A \iff x \notin x$
{{AimForCont}} $A$ were a set.
Then we could set $A$ for $x$, and so obtain:
:$A \in A \iff A \notin A$
This is a contradiction.
Hence by Proof by Contradiction $A$ cannot be a set.
But as $A$ is a subclass of the universal class $V$, $A$ is a class.
So the class $A$ of ordinary sets is not a set.
That is:
:$A \notin V$
{{qed}}
Theorem: Not Every Class is a Set

Let $A$ be a class.
Then it is not necessarily the case that $A$ is also a set.

Proof:
Suppose $A$ is the universal class, which is {{afortiori}} a class.
The result follows from Basic Universe is not Set.
{{qed}}
Theorem: Class has Subclass which is not Element

Let $A$ be a class.
Then $A$ has at least one subclass $B$ which is not an element of $A$.

Proof:
Let a set $x$ be defined as '''ordinary''' {{iff}} $x \notin x$.
Let $\map \phi x$ be the set property defined as:
:$\map \pi x := \neg \paren {x \in x}$
Then by the {{Axiom-link|Specification|Classes}} there exists a class, which can be denoted $B$, such that:
:$B = \set {x \in A: \neg \paren {x \in x} }$
That is, $B$ contains as elements of all the '''ordinary''' sets of $A$.
By the {{Axiom-link|Extension|Classes}} $B$ is unique.
Thus $B$ is the class of all '''ordinary''' sets of $A$.
:$x \in B \iff \paren {x \in A \land x \notin x}$
Hence, for all $x$ which happen to be elements of $A$, we have:
:$x \in B \iff x \notin x$
{{AimForCont}} $B \in A$.
Then we could set $A$ for $x$, and so obtain:
:$B \in B \iff B \notin B$
This is a contradiction.
Hence by Proof by Contradiction $B$ cannot be an element of $A$.
That is:
:$B \notin V$
{{qed}}
Theorem: Basic Universe is Supercomplete

Let $V$ be a basic universe.
Then $V$ is supercomplete.

Proof:
By definition, a class $V$ is supercomplete {{iff}} $V$ is both transitive and swelled.
From the {{axiom-link|Transitivity}}, $V$ is transitive.
From the {{axiom-link|Swelledness}}, $V$ is swelled.
Hence the result.
{{qed}}
Theorem: Basic Universe is not Set

Let $V$ be a basic universe.
Then $V$ is not a set.

Proof:
{{AimForCont}} $V$ were a set.
Then by the the {{axiom-link|Swelledness}}, $V$ is swelled.
That is, as $V$ is a set, every subclass of $V$ would also be a set.
From Class has Subclass which is not Element, $V$ has a subclass $S$ which is not an element of $V$.
That is:
:$\exists S \subseteq V: S \notin V$
But by definition of a basic universe, $V$ is a universal class.
That is:
:$S \in V$
This contradicts the deduction that $S \notin V$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Empty Class Exists and is Unique

There is exactly one empty class.

Proof:
Let $P$ be a property such that $\map P x$ is satisfied by no $x$ at all, for example:
:$\forall x: \map P x := \neg {x = x}$
Then by the Axiom of Specification we can create the class $A$ such that:
:$A := \set {x \in V \land \neg {x = x} }$
from which it is seen that $A$ has no elements.
Hence there exists an empty class.
Let $A$ and $B$ both be empty classes.
By definition, both $A$ and $B$ contain the same elements, that is, no elements at all.
By the Axiom of Extension, that means $A = B$.
Hence the result.
{{qed}}
Theorem: Empty Class is Subclass of All Classes

The empty class is a subclass of all classes.

Proof:
Let $A$ be a class.
By definition of the empty class:
:$\forall x: \neg \paren {x \in \O}$
From False Statement implies Every Statement:
:$\forall x: \paren {x \in \O \implies x \in A}$
Hence the result by definition of subclass.
{{qed}}
Theorem: Empty Class is Supercomplete

The empty class is supercomplete.

Proof:
Vacuously, every element of $\O$ is also a subclass of $\O$.
Hence $\O$ is transitive by definition.
Vacuously, every subclass of every element of $\O$ is also an element of $\O$.
Hence $\O$ is swelled by definition.
The result follows by definition of supercomplete.
{{qed}}
Theorem: Basic Universe is not Empty

Let $V$ be a basic universe
Then $V$ is not the empty class.

Proof:
The {{axiom-link|the Empty Set|Class Theory}} gives us:
{{:Axiom:Axiom of the Empty Set (Class Theory)}}
Hence the result by definition of empty class.
{{Qed}}
Theorem: Existence of Set is Equivalent to Existence of Empty Set

Let $V$ be a basic universe.
Let $P$ be the axiom:
:$V$ has at least one element.
Then $P$ is equivalent to the {{axiom-link|the Empty Set|Class Theory}}:
:The empty class $\O$ is a set.

Proof:
=== Necessary Condition ===
Let the {{axiom-link|the Empty Set|Class Theory}} hold.
That is:
:$\O$ is a set.
By definition of a basic universe, $V$ is a universal class.
Hence, by definition, every set is an element of $V$.
We have that $\O$ is a set {{hypothesis}}.
Thus:
:$\O \in V$
and by definition of empty class it is seen that $V$ is not empty.
{{qed|lemma}}
Theorem: Singleton Class can be Formed from Set

Let $V$ be a basic universe.
Let $a \in V$ be a set.
Then the singleton class $\set a$ can be formed, which is a subclass of $V$.

Proof:
Using the axiom of specification, let $A$ be the class defined as:
:$A := \set {x: x \in V \land x = a}$
That is:
:$A = \set a$
By the axiom of extension, $\set a$ is the only such class which has $a$ as an element.
Theorem: Singleton Class of Empty Set is Supercomplete

Let $\O$ denote the empty set.
Then the singleton $\set \O$ is supercomplete.

Proof:
Let $x \in \set \O$ be any element of $\set \O$.
Then it has to be the case that $x = \O$.
Then every element of $\O$ is an element of $\set \O$ vacuously.
That is, $\set \O$ is swelled.
There is one element of $\set \O$, and that is $\O$.
This is a subclass of $\set \O$.
That is, $\set \O$ is transitive.
The result follows by definition of supercomplete class.
{{qed}}
Theorem: Singleton Classes are Equal iff Sets are Equal

Let $a$ and $b$ be sets.
Let $\set a$ and $\set b$ denote the singleton classes of $a$ and $b$.
Then:
:$\set a = \set b \iff a = b$

Proof:
Let $a = b$.
Then $\set a$ and $\set b$ contain the same elements.
Hence by the axiom of extension it follows that $\set a = \set b$.
Let $\set a = \set b$.
We have that $a \in \set a$.
As $\set a = \set b$ we also have that $a \in \set b$.
But $b$ is the only element of $\set b$.
Hence it must be the case that $a = b$.
{{qed}}
Theorem: Doubleton Class can be Formed from Two Sets

Let $V$ be a basic universe.
Let $a, b \in V$ be sets.
Then the doubleton class $\set {a, b}$ can be formed, which is a subclass of $V$.

Proof:
Using the {{Axiom-link|Specification|Classes}}, let $A$ be the class defined as:
:$A := \set {x: x \in V \land \paren {x = a \lor x = b} }$
That is:
:$A = \set {a, b}$
By the {{Axiom-link|Extension|Classes}}, $\set {a, b}$ is the only such class which has $a$ and $b$ as elements.
Theorem: Doubleton Class of Equal Sets is Singleton Class

Let $V$ be a basic universe.
Let $a, b \in V$ be sets.
Consider the doubleton class $\set {a, b}$.
Let $a = b$.
Then:
:$\set {a, b} = \set a$
where $\set a$ denotes the singleton class of $a$.

Proof:
Let $A = \set {a, b}$
The existence of $A$ is shown in Doubleton Class can be Formed from Two Sets:
:$A := \set {x: \paren {x = a \lor x = b} }$
Let $a = b$.
Then:
{{begin-eqn}}
{{eqn | l = A
      | r = \set {a, b}
      | c = Definition of $A$
}}
{{eqn | r = \set {a, a}
      | c = as $a = b$
}}
{{eqn | ll= \leadsto
      | l = x \in \set {a, a}
      | o = \iff
      | r = \paren {x = a \lor x = a}
      | c = Definition of $A$
}}
{{eqn | ll= \leadsto
      | l = x \in \set {a, a}
      | o = \iff
      | r = x = a
      | c = Rule of Idempotence
}}
{{eqn | ll= \leadsto
      | l = x \in \set {a, a}
      | o = \iff
      | r = x \in \set a
      | c = {{Defof|Singleton Class}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Formulations of Axiom of Pairing

The following formulations of the '''{{axiom-link|Pairing|Set Theory}}''' in the context of '''axiomatic set theory''' are equivalent:

Proof:
=== Strong Form implies Weak Form ===
Let the strong form of the Axiom of Pairing be assumed:
{{:Axiom:Axiom of Pairing/Set Theory/Strong Form}}
By definition of the biconditional, this can be expressed as:
:$\forall a: \forall b: \exists c: \forall z: \paren {\paren {z = a \lor z = b \implies z \in c} \land \paren {z \in c \implies z = a \lor z = b} }$
from which, by the Rule of Simplification:
:$\forall a: \forall b: \exists c: \forall z: \paren {z = a \lor z = b \implies z \in c}$
Thus the weak form of the Axiom of Pairing is seen to hold.
{{qed|lemma}}
Theorem: Singleton Class of Set is Set

Let $x$ be a set.
Then the singleton class $\set x$ is likewise a set.

Proof:
Let $x$ and $y$ be sets.
Let $x = y$.
From Doubleton Class of Equal Sets is Singleton Class, the doubleton class $\set {x, y}$  is the singleton class $\set x$.
From the axiom of pairing, the doubleton class $\set {x, y}$ is a set when $x$ and $y$ are sets.
Hence $\set x$ is a set.
{{qed}}
Theorem: Basic Universe has Infinite Number of Elements

Let $V$ be a basic universe.
Then $V$ has an infinite number of elements.

Proof:
Let $a_n$ be the class defined as:
:$\forall n \in \N: a_n = \begin{cases} \O & : n = 0 \\ \set {a_{n - 1} } & : n > 0 \end {cases}$
It is shown by the Principle of Mathematical Induction that $a_n$ is a set for all $n \in \N$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a_n$ is a set.
Theorem: Equivalence of Formulations of Axiom of Pairing for Classes

The following formulations of the '''{{axiom-link|Pairing}}''' in the context of '''class theory''' are equivalent:

Proof:
It is assumed that all classes are subclasses of a basic universe $V$.
Theorem: Equality of Ordered Pairs/Lemma

Let $\set {a, b}$ and $\set {a, d}$ be doubletons such that $\set {a, b} = \set {a, d}$.
Then:
:$b = d$

Proof:
We have that:
:$b \in \set {a, b}$
and so by definition of set equality:
:$b \in \set {a, d}$
So:
:$(1): \quad$ either $b = a$ or $b = d$.
First suppose that $b = a$.
Then:
:$\set {a, b} = \set {a, a} = \set a$
We have that:
:$d \in \set {a, d}$
and so by definition of set equality:
:$d \in \set {a, b}$
and so as $\set {a, b} = \set a$ it follows that:
:$d = a$
We have $b = a$ and $d = a$, and so:
:$b = d$
{{qed|lemma}}
Next suppose that $b \ne a$.
We have from $(1)$ that either $b = a$ or $b = d$.
As $b \ne a$ it must be the case that $b = d$.
{{qed|lemma}}
So in either case we see that:
:$b = d$
{{qed}}
Theorem: Equality of Ordered Pairs/Necessary Condition

Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs such that $\tuple {a, b} = \tuple {c, d}$.
Then $a = c$ and $b = d$.

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the empty set formalization:
:$\set {\set {\O, a}, \set {\set \O, b} } = \set {\set {\O, c}, \set {\set \O, d} }$
First we note the special case where $a = \set \O$ and $b = \O$.
Then we have:
{{begin-eqn}}
{{eqn | l = \set {\set {\O, a}, \set {\set \O, b} }
      | r = \set {\set {\O, \set \O}, \set {\set \O, \O} }
      | c = 
}}
{{eqn | r = \set {\set {\O, \set \O}, \set {\O, \set \O} }
      | c = {{Defof|Set Equality}}: $\set {\O, \set \O } = \set {\set \O, \O}$
}}
{{eqn | r = \set {\set {\O, \set \O} }
      | c = Doubleton Class of Equal Sets is Singleton Class
}}
{{eqn | r = \set {\set {\O, c}, \set {\set \O, d} }
      | c = by definition
}}
{{end-eqn}}
Thus we have that:
:$c = d = \set {\O, \set \O}$
and so:
:$c = \set \O$ and $d = \O$
leading to the result that $a = c$ and $b = d$.
{{qed|lemma}}
Suppose otherwise, that either $a \ne \set \O$ or $b \ne \O$, or both.
Let $x \in \set {\set {\O, a}, \set {\set \O, b} }$.
Then either:
:$x = \set {\O, a}$
or:
:$x = \set {\set \O, b}$
First suppose $x = \set {\O, a}$.
Then:
:$x = \set {\O, c}$ or $x = \set {\set \O, d}$
{{AimForCont}} $x = \set {\set \O, d}$.
That is:
:$\set {\O, a} = \set {\set \O, d}$
which means that $a = \set \O$ and $d = \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\set \O, d}$.
Thus $x = \set {\O, c}$.
We have that:
:$x = \set {\O, a}$ and $x = \set {\O, c}$
and so:
:$\set {\O, a} = \set {\O, c}$
It follows from the lemma that:
:$a = c$
Now suppose $x = \set {\set \O, b}$.
Then:
:$x = \set {\O, c} \lor \set {\set \O, d}$
{{AimForCont}} $x = \set {\O, c}$.
That is:
:$\set {\set \O, b} = \set {\O, c}$
which means that $b = \O$ and $c = \set \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, c}$.
Thus $x = \set {\set \O, d}$.
We have that:
:$x = \set {\set \O, b}$ and $x = \set {\set \O, d}$
and so:
:$\set {\set \O, b} = \set {\set \O, d}$
It follows from the lemma that:
:$b = d$
{{qed}}
Theorem: Equality of Ordered Pairs/Necessary Condition

Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs such that $\tuple {a, b} = \tuple {c, d}$.
Then $a = c$ and $b = d$.

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the Kuratowski formalization:
:$\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} }$ 
There are two cases: either $a = b$, or $a \ne b$.
==== Case 1 ====
Suppose $a = b$.
Then:
:$\set {\set a, \set {a, b} } = \set {\set a, \set a} = \set {\set a}$
Thus $\set {\set c, \set {c, d} }$ has only one element.
Thus $\set c = \set {c, d}$ and so $c = d$.
So:
:$\set {\set c, \set {c, d} } = \set {\set a}$
and so $a = c$ and $b = d$.
Thus the result holds.
{{qed|lemma}}
==== Case 2 ====
Now suppose $a \ne b$. By the same argument it follows that $c \ne d$.
So that means that either $\set a = \set c$ or $\set a = \set {c, d}$.
Since $\set {c, d}$ has $2$ distinct elements, $\set a \ne \set {c, d}$.
Thus:
:$\set a = \set c$
and so $a = c$.
Then:
:$\set {a, b} = \set {c, d}$
But as $a = c$ that means we have:
:$\set {a, b} = \set {a, d}$
It follows from the lemma that:
:$b = d$
{{qed}}