nyuuzyou/wikis huggingface dataset:
Axes of Symmetry of Hyperbola

== Theorem ==
The hyperbola has $2$ axis of bilateral symmetry:
:the transverse axis
:the conjugate axis.
When expressed in reduced form in a cartesian plane, these correspond respectively with the $x$-axis and the $y$-axis.
== Proof ==
== Sources ==
* 
* 
Category:Hyperbolas
Category:Bilateral Symmetry
Axes of Symmetry of Kappa Curve

== Theorem ==
Let $\KK$ be a kappa curve expressed in Cartesian coordinates as:
:$x^4 + x^2 y^2 = a^2 y^2$
$\KK$ has two axis of bilateral symmetry:
:the $x$-axis
:the $y$-axis.
:
== Proof ==
== Sources ==
* 
* 
Category:Kappa Curve
Category:Bilateral Symmetry
Axiom of Approximation in Up-Complete Semilattice

== Theorem ==
Let $\mathscr S = \struct {S, \wedge, \preceq}$ be an up-complete meet semilattice.
Let:
:$\forall x \in S: x^\ll$ is directed
Then:
:$\mathscr S$ satisfies the axiom of approximation
:
:$\forall x, y \in S: x \npreceq y \implies \exists u \in S: u \ll x \land u \npreceq y$
== Proof ==
=== Sufficient Condition ===
Let $\mathscr S$ satisfy the axiom of approximation.
Let $x, y \in S$ such that
:$x \npreceq y$
By assumption:
:$x^\ll$ is directed.
By definition of up-complete:
:$x^\ll$ admits a supremum.
By the axiom of approximation:
:$x = \map \sup {x^\ll}$
By definition of supremum:
:if $y$ is upper bound for $x^\ll$, then $x \preceq y$
By definition of upper bound:
:$\exists u \in x^\ll: u \npreceq y$
Thus by definition of way below closure:
:$\exists u \in S: u \ll x \land u \npreceq y$
=== Necessary Condition ===
Let:
:$\forall x, y \in S: x \npreceq y \implies \exists u \in S: u \ll x \land u \npreceq y$
Let $x \in S$.
By assumption:
:$x^\ll$ is directed.
By definition of up-complete:
:$x^\ll$ admits a supremum.
By Operand is Upper Bound of Way Below Closure:
:$x$ is upper bound for $x^\ll$
We will prove that:
:$\forall y \in S: y$ is upper bound for $x^\ll \implies x \preceq y$
Let $y \in S$ such that:
:$y$ is upper bound for $x^\ll$
:
:$x \npreceq y$
By assumption:
:$\exists u \in S: u \ll x \land u \npreceq y$
By definition of way below closure:
:$u \in x^\ll$
By definition of upper bound
:$u \preceq y$
This contradicts $u \npreceq y$
Thus by definition of supremum:
:$x = \map \sup {x^\ll}$
Thus by definition:
:$\mathscr S$ satisfies the axiom of approximation.
== Sources ==
* 
* 
Category:Way Below Relation
Category:Up-Complete Semilattices
Axiom of Archimedes

== Theorem ==
Let $x$ be a real number.
Then there exists a natural number greater than $x$.
:$\forall x \in \R: \exists n \in \N: n > x$
That is, the set of natural numbers is unbounded above.
=== Variant ===
== Proof ==
Let $x \in \R$.
Let $S$ be the set of all natural numbers less than or equal to $x$:
:$S = \set {a \in \N: a \le x}$
It is possible that $S = \O$.
Suppose $0 \le x$.
Then by definition, $0 \in S$.
But $S = \O$, so this is a contradiction.
From the Trichotomy Law for Real Numbers it follows that $0 > x$.
Thus we have the element $0 \in \N$ such that $0 > x$.
Now suppose $S \ne \O$.
Then $S$ is bounded above (by $x$, for example).
Thus by the Continuum Property of $\R$, $S$ has a supremum in $\R$.
Let $s = \map \sup S$.
Now consider the number $s - 1$.
Since $s$ is the supremum of $S$, $s - 1$ cannot be an upper bound of $S$ by definition.
So $\exists m \in S: m > s - 1 \implies m + 1 > s$.
But as $m \in \N$, it follows that $m + 1 \in \N$.
Because $m + 1 > s$, it follows that $m + 1 \notin S$ and so $m + 1 > x$.
== Also known as ==
== Also see ==
* The Archimedean property, which may or may not be satisfied by an abstract algebraic structure.
* In Equivalence of Archimedean Property and Archimedean Law it is shown that on the field of real numbers the two are equivalent.
Not to be confused with the better-known (outside the field of mathematics) Archimedes' Principle.
== Historical Note ==
== Sources ==
* : $1$: Review of some real analysis: $\S 1.1$: Real Numbers: Proposition $1.1.6$
* : $\S 3$: Natural Numbers: $\S 3.3$: Archimedean Property
* 
* : $1$: Set Theory and Logic: $\S 4$: The Integers and the Real Numbers
* 
* 
* 
Category:Axiom of Archimedes
Category:Real Analysis
Category:Number Theory
Axiom of Archimedes/Also known as

== Axiom of Archimedes: Also known as ==
The Axiom of Archimedes is also known as:
* the Archimedean Law
* the Archimedean Property (of the natural numbers)
* the Archimedean Ordering Property (of the real line)
* the Archimedean Principle
* Archimedes' Axiom.
== Sources ==
* : $1$: Review of some real analysis: $\S 1.1$: Real Numbers: Proposition $1.1.6$
* : $\S 3$: Natural Numbers: $\S 3.3$: Archimedean Property
* : $1$: Set Theory and Logic: $\S 4$: The Integers and the Real Numbers
* 
* 
* 
Category:Axiom of Archimedes
Axiom of Archimedes/Historical Note

== Historical Note on the Axiom of Archimedes ==
The Axiom of Archimedes appears as Axiom $\text V$ of ' .
It also appears in his , where he words it (up to translation) as:
:the excess by which the greater of (two) unequal areas exceeds the less can, by being added to itself, be made to exceed any given finite area.
The name Axiom of Archimedes was given by in his $1882$ work: Zur Geometrie der Alten, insbesondere über ein Axiom des Archimedes.
== Sources ==
* 
* 
Category:Historical Notes
Axiom of Archimedes/Variant

== Theorem ==
Let $x$ and $y$ be a natural numbers.
Then there exists a natural number $n$ such that:
:$n x \ge y$
== Proof ==
 there exists $x, y \in \N$ such that $n x < y$ for every natural number $n$.
Consider the set $S$, defined as:
:$S := \set {y - n x: n \in \N}$
We have that $S$ contains only natural numbers.
By the Well-Ordering Principle, $S$ contains a smallest element, $y - m x$ for example.
But $y - \paren {m + 1} x$ is also in $S$, as $S$ contains all natural numbers of this form.
Furthermore, we have:
:$y - \paren {m + 1} x = \paren {y - m x} - x < y - m x$
But this contradicts our assertion that $y - m x$ is the smallest element of $S$.
This assertion originated from the assumption that there exists $x, y \in \N$ such that $n x < y$ for every natural number $n$.
Hence that assumption cannot hold.
Hence the result by Proof by Contradiction.
== Sources ==
* : Chapter $1$: Some Preliminary Considerations: $1.1$ Mathematical Induction: Theorem $1 \text{-} 1$
Category:Axiom of Archimedes
Axiom of Choice/Examples/Russell's Socks and Shoes

== Example of Use of Axiom of Choice ==
Suppose we have an infinite number of pairs of socks.
Using the , we can simultaneously pick one sock from each pair.
However, if we also have a infinite number of pairs of shoes, we no longer need the to pick one shoe from each pair.
We simply choose the left one.
== Proof ==
This is more formally stated as:
:Given an infinite set of unordered pairs, the is needed to pick one element from each pair.
:Given an infinite set of ordered pairs, the is not needed to pick one element from each of the pairs: we may simply pick the first element of each.
== Historical Note ==
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text I$ -- Superinduction and Well Ordering: $\S 1$ Introduction to well ordering
Category:Examples of Use of Axiom of Choice
Axiom of Choice/Examples/Russell's Socks and Shoes/Historical Note

== Historical Note on Russell's Socks and Shoes ==
This example was devised by as a neat illustration of how the can be used.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text I$ -- Superinduction and Well Ordering: $\S 1$ Introduction to well ordering
Category:Historical Notes
Axiom of Choice Implies Axiom of Dependent Choice

== Theorem ==
The axiom of choice implies the axiom of dependent choice.
== Proof ==
Let $\RR$ be a binary endorelation on a non-empty set $S$ such that:
:$\forall a \in S: \exists b \in S: a \mathrel \RR b$
For an element $x \in S$, define:
:$\map R x = \set {y \in S: x \mathrel \RR y}$
By assumption, $\map R x$ is non-empty for all $x \in S$.
Now, consider the indexed family of sets:
:$\family {\map R x}_{x \mathop \in S}$
Using the axiom of choice, there exists a mapping $f: S \to S$ such that:
:$\forall x \in S: \map f x \in \map R x$
That is:
:$x \mathrel \RR \map f x$
So, for any $x \in S$, the sequence:
:$\sequence {x_n}_{n \mathop \in \N} = \sequence {\map {f^n} x}_{n \mathop \in \N}$
where $f^n$ denotes the composition of $f$ with itself $n$ times, is a sequence such that:
:$x_n \mathrel \RR x_{n + 1}$
for all $n \in \N$, as desired.
== Also see ==
* Axiom of Dependent Choice Implies Axiom of Countable Choice
Category:Axiom of Dependent Choice
Category:Axiom of Choice
Axiom of Choice implies Hausdorff's Maximal Principle

== Theorem ==
Let the Axiom of Choice be accepted.
Then Hausdorff's Maximal Principle holds.
=== Statement of Axiom of Choice ===
=== Statement of Hausdorff's Maximal Principle ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
Category:Hausdorff's Maximal Principle
Category:Axiom of Choice
Category:Axiom of Choice implies Hausdorff's Maximal Principle
Axiom of Choice implies Hausdorff's Maximal Principle/Proof 1

== Theorem ==
== Proof ==
Let $S$ be the set of all chains of $\PP$.
$S \ne \O$ since the empty set is an element of $S$. 
From Subset Relation is Ordering, we have that $\struct {S, \subseteq}$ is partially ordered by inclusion.
Let $C$ be a totally ordered subset of $\struct {S, \subseteq}$.
Then $\bigcup C$ is a chain in $C$ by Set of Chains is Closed under Chain Unions under Subset Relation.
This shows that $S$, ordered by set inclusion, is an inductive ordered subset.
By applying Zorn's Lemma, the result follows.
Category:Axiom of Choice implies Hausdorff's Maximal Principle
Axiom of Choice implies Hausdorff's Maximal Principle/Proof 2

== Theorem ==
== Proof ==
Let $\preceq$ be an ordering on the set $\PP$.
Let $X$ be a chain in $\struct {\PP, \preceq}$.
By definition, a maximal chain in $\PP$ that includes $X$ is a chain $Y$ in $\PP$ such that $X \subseteq Y$ and there is no chain $Z$ in $\PP$ with $X \subseteq Z$ and $Y \subsetneq Z$.
Let us define $\CC$ as:
:$\CC = \leftset {Y : Y}$ is a chain in $\PP$ and $\rightset {X \subseteq Y}$
Then:
:a maximal chain in $\PP$ that includes $X$
and:
:a maximal element of $\CC$ under the partial order induced on $\CC$ by inclusion
are one and the same.
It thus suffices to show that $\CC$ contains such a maximal element.
According to Zorn's Lemma, $\CC$ contains a maximal element if each chain in $\CC$ has an upper bound in $\CC$.
Let $W$ be an arbitrary chain in $\CC$.
Let $Z = \bigcup W$.
It will be shown that $Z$ is an upper bound for $W$ in $\CC$.
Let $a, b \in Z$.
Then:
:$\exists A, B \in W: a \in A, b \in B$
Since $W$ is a chain in $\CC$, one of $A$ and $B$ includes the other.
, suppose $A \subseteq B$.
Then $a, b \in B$.
Since $B$ is a chain in $\PP$, either $a \preceq b$ or $b \preceq a$.
Therefore $Z$ is a chain in $\PP$.
By definition of $Z$, we have that:
:$\forall A \in W: A \subseteq Z$
Thus $Z$ is an upper bound for $W$ under inclusion.
Finally we have that:
:$\forall A \in W: X \subseteq A$
and so $X \subseteq Z$.
Thus:
:$Z \in \CC$
We have shown that for an arbitrary chain $W$ in $\CC$, $W$ has an upper bound $Z$ in $\CC$.
The result follows.
Category:Axiom of Choice implies Hausdorff's Maximal Principle
Axiom of Choice implies Hausdorff's Maximal Principle/Proof 3

== Theorem ==
== Proof ==
Let $\struct {\CC, \subseteq}$ be the set of all chains in $P$ ordered by inclusion. 
By Set of Chains is Closed under Chain Unions under Subset Relation, $\CC$ is a chain complete ordered set.
Now define $f: \CC \to \CC$ as follows:
:If $C$ is a maximal chain then $\map f C = C$.
:Otherwise $f$ chooses arbitrarily, using the axiom of choice, some chain $D$ which strictly contains $C$.
By construction, $\map f C \supseteq C$.
By the above, $\CC$ is chain complete.
Therefore the Bourbaki-Witt Fixed Point Theorem applies and $f$ has a fixed point $\map F M = M$.
But by the above construction, the only fixed points of $f$ are maximal chains.
Therefore $M$ is a maximal chain.
Category:Axiom of Choice implies Hausdorff's Maximal Principle
Axiom of Choice implies Kuratowski's Lemma

== Theorem ==
Let the Axiom of Choice be accepted.
Then Kuratowski's Lemma holds.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles: Theorem $5.2$
Category:Kuratowski's Lemma
Category:Axiom of Choice
Category:Axiom of Choice implies Kuratowski's Lemma
Axiom of Choice implies Kuratowski's Lemma/Proof 2

== Theorem ==
== Proof ==
Recall Kuratowski's Lemma:
By the Axiom of Choice, there exists a choice function for $S$.
By Closed Set under Chain Unions with Choice Function is of Type $M$:
:every element of $S$ is a subset of a maximal element of $S$ under the subset relation.
Hence the result.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles: Theorem $5.2$
Category:Axiom of Choice implies Kuratowski's Lemma
Axiom of Choice implies Maximal Principles

== Theorem ==
Let the Axiom of Choice be accepted.
Then the Maximal Principles hold.
== Proof ==
From Maximal Principles are Equivalent, it is sufficient to demonstrate that any one of them is implied by the Axiom of Choice.
Indeed, we have several such theorems:
* Axiom of Choice implies Kuratowski's Lemma
* Axiom of Choice implies Tukey's Lemma
* Axiom of Choice implies Zorn's Lemma
* Axiom of Choice implies Hausdorff's Maximal Principle
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles
Category:Maximal Principles
Category:Axiom of Choice
Axiom of Choice implies Tukey's Lemma

== Theorem ==
Let the Axiom of Choice be accepted.
Then Tukey's Lemma holds.
== Proof ==
Let us assume the truth of the Axiom of Choice.
From Axiom of Choice implies Kuratowski's Lemma, it follows that Kuratowski's Lemma holds.
From Kuratowski's Lemma implies Tukey's Lemma, it follows that Tukey's Lemma holds.
Hence the result.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles: Proposition $5.6$
Category:Axiom of Choice
Category:Tukey's Lemma
Axiom of Choice implies Zorn's Lemma

== Theorem ==
Let the be accepted.
Then Zorn's Lemma holds.
=== Statement of ===
=== Statement of Zorn's Lemma ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Also see ==
* Maximal Principles
Category:Axiom of Choice
Category:Zorn's Lemma
Category:Axiom of Choice implies Zorn's Lemma
Axiom of Choice implies Zorn's Lemma/Proof 2

== Theorem ==
== Proof ==
 that for each $x \in X$ there is a $y \in X$ such that $x \prec y$.
By the Axiom of Choice, there is a mapping $f: X \to X$ such that:
:$\forall x \in X: x \prec \map f x$
Let $\CC$ be the set of all chains in $X$.
By the premise, each element of $\CC$ has an upper bound in $X$.
Thus by the Axiom of Choice, there is a mapping $g: \CC \to X$ such that for each $C \in \CC$, $\map g C$ is an upper bound of $C$.
Let $p$ be an arbitrary element of $X$.
Define a mapping $h: \On \to X$ by transfinite recursion thus:
when $h \sqbrk \lambda$ is the image set of $\lambda$ under $h$.
Then $h$ is strictly increasing, and thus injective.
Let $h'$ be the restriction of $h$ to $\On \times \map h \On$.
Then ${h'}^{-1}$ is a surjection from $\map h \On \subseteq X$ onto $\On$.
By the Axiom of Replacement, $\On$ is a set.
By the Burali-Forti Paradox, this is a contradiction.
Thus we conclude that some element of $X$ has no strict successor, and is thus maximal.
Category:Axiom of Choice implies Zorn's Lemma
Axiom of Choice implies Zorn's Lemma/Proof 3

== Theorem ==
== Proof ==
We have that Axiom of Choice implies Tukey's Lemma.
Then we have Tukey's Lemma implies Zorn's Lemma.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles: Proposition $5.8$
Category:Axiom of Choice implies Zorn's Lemma
Axiom of Choice is Independent of ZF/Historical Note

== Historical Note on Axiom of Choice is Independent of ZF ==
 showed that the Axiom of Choice is not disprovable in Zermelo-Fraenkel set theory.
 showed that neither is the Axiom of Choice provable in Zermelo-Fraenkel set theory.
== Sources ==
* : Chapter $1$: General Background: $\S 5$ The continuum problem
Category:Historical Notes
Axiom of Dependent Choice Implies Axiom of Countable Choice

== Theorem ==
The axiom of dependent choice implies the axiom of countable choice.
== Proof ==
Let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of non-empty sets.
Define:
:$\ds S = \bigsqcup_{n \mathop \in \N} S_n$
where $\bigsqcup$ denotes disjoint union.
Let $\RR$ be the binary endorelation on $S$ defined by:
:$\tuple {x, m} \mathrel \RR \tuple {y, n} \iff n = m + 1$
Note that $\RR$ satisfies:
:$\forall a \in S : \exists b \in S : a \mathrel \RR b$
Using the axiom of dependent choice, there exists a sequence $\sequence {y_n}_{n \mathop \in \N}$ in $S$ such that $y_n \mathrel \RR y_{n + 1}$ for all $n \in \N$.
Letting $y_n = \tuple {s_n, N_n}$ for all $n \in \N$, it follows by the definition of $\RR$ that $N_{n + 1} = N_n + 1$.
A straightforward application of mathematical induction shows that $N_n = n + N$ for some $N \in \N$.
So $s_n \in S_{n + N}$ for all $n \in \N$.
The cartesian product $S_0 \times S_1 \times \cdots \times S_{N - 1}$ is non-empty.
So there exists a finite sequence $x_0, x_1, \ldots, x_{N - 1}$ with $x_n \in S_n$ for all natural numbers $n < N$.
Now, define $x_n = s_{n - N}$ for all natural numbers $n \ge N$.
Then $x_n \in S_n$ for all $n \in \N$.
== Also see ==
* Axiom of Choice Implies Axiom of Dependent Choice
Category:Axiom of Dependent Choice
Category:Axiom of Countable Choice
Axiom of Foundation (Strong Form)/Proof 1

== Theorem ==
== Proof ==
By Epsilon Relation is Strictly Well-Founded, $\Epsilon$, the epsilon relation, is a strictly well-founded relation on $B$.
By Epsilon Relation is Proper, $\struct {\mathbb U, \Epsilon}$ is a proper relational structure, where $\mathbb U$ is the universal class.
By Well-Founded Proper Relational Structure Determines Minimal Elements, $B$ has a strictly minimal element under $\Epsilon$.
== Sources ==
* : $\S 9.20$
Category:Axiom of Foundation (Strong Form)
Axiom of Foundation (Strong Form)/Proof 2

== Theorem ==
== Proof ==
Let $x \in B$.
Let $x'$ be the transitive closure of $x$.
Let $L = x' \cap B$.
Then $x \in L$, so $L$ is not empty.
Since $x'$ is a set, so is $L$, by the axiom of subset.
Thus by the Axiom of Foundation, $L$ has an $\in$-minimal element $m$.
By the definition of intersection, $m \in B$.
 that there is an element $b \in B$ such that $b \in m$.
Then since $m \in x'$ and $x'$ is transitive, $b \in x'$.
Thus $b \in L$, contradicting the minimality of $m$.
So $m$ is an $\in$-minimal element of $B$.
Category:Axiom of Foundation (Strong Form)
Axiom of Pairing from Axiom of Specification

== Theorem ==
Let it be supposed that there exists a set which contains at least two elements.
Then the Axiom of Pairing is a consequence of the Axiom of Specification.
== Proof ==
Let $A$ be a set which contains at least two elements.
Let $a$ and $b$ be any two elements of $A$.
Let $\map P x$ be the propositional function:
:$\map P x := \paren {x = a \lor x = b}$
Then we may use the Axiom of Specification to define $B$ as:
:$x \in B \iff \set {x \in A: \map P x}$
Hence we can define:
:$B := \set {a, b}$
for any two $a, b \in A$.
== Sources ==
* : $\S 3$: Unordered Pairs
Category:Axiom of Pairing
Category:Doubletons
Axiom of Pairing from Infinity and Replacement

== Theorem ==
The Axiom of Pairing is a consequence of:
:the Axiom of Infinity
and
:the Axiom of Replacement.
== Proof ==
The set $2 = \set {\O, \set \O}$ is used with the Axiom of Replacement as the domain for a mapping whose image is $\set {A, B}$.
A suitable mapping would be:
:$\paren {y = \O \land z = A} \lor \paren {y = \set \O \land z = B}$
The set $2$ is shown to exist as a member of the infinite set whose existence is asserted by the axiom of infinity.
Category:Axiom of Pairing
Category:Doubletons
Axiom of Pairing from Powers and Replacement

== Theorem ==
The is a consequence of:
:the 
and
:the 
and also
:the .
== Proof ==
It is to be shown that $2 = \set {\O, \set \O}$ is a set.
By the , it is seen that $\O$ is a set.
By the , it is seen that $\powerset \O$ is also a set.
It is to be shown that $\powerset \O = \set \O$.
To determine the elements of $\powerset \O$, we must find all of the sets $z$ such that:
:$\forall x: x \in z \implies x \in \O$
From the definition of the empty set, the of this expression is invariably false.
So by Rule of Transposition, we deduce that:
:$\forall x: x \notin z$
But this is the definition of the empty set.
So by Empty Set is Unique, it follows that $\powerset \O = \set \O$.
It is now to be shown that $\powerset {\set \O} = \set {\O, \set \O}$.
By Empty Set is Subset of All Sets, $\O \in \powerset {\set \O}$.
By Set is Subset of Itself, $\set \O \in \powerset {\set \O}$.
And so:
:$(1) \quad \set {\O, \set \O} \subseteq \powerset {\set \O}$
It is now to be shown that $\set {\O, \set \O} \supseteq \powerset {\set \O}$.
 that there exists a set $S \in \powerset {\set \O}$ such that $S \ne \O$ and $S \ne \set \O$.
But then $\exists x \ne \O: x \in \set \O$, which is false.
Therefore by contradiction:
:$(2) \quad \powerset {\set \O} \subseteq \set {\O, \set \O}$.
Putting $(1)$ and $(2)$ together yields:
:$\powerset {\set \O} = \set {\O, \set \O}$
The set $2 = \set {\O, \set \O}$ is used with the as the domain for a mapping whose image is $\set {A, B}$.
A suitable mapping would be:
:$\paren {y = \O \land z = A} \lor \paren {y = \set \O \land z = B}$
Usually this mapping would be written as:
:$\map f x = \begin{cases}
A & : x = \O \\
B & : x = \set \O
\end{cases}$
Category:Axiom of Pairing
Category:Doubletons
Axiom of Replacement implies Image of Bijection on Set is Set

== Theorem ==
Let the Axiom of Replacement (in the context of class theory) be accepted.
Let $A$ be a class which can be put into one-to-one correspondence with a set.
Then $A$ is a set.
== Proof ==
Let $x$ be a set such that $A$ can be put into one-to-one correspondence with $x$.
Then by definition there exists a bijection from $x$ to $A$.
Let $f: x \to A$ be such a bijection.
Then by the Axiom of Replacement, $f \sqbrk x$ is a set.
But:
:$f \sqbrk x = A$
Hence the result.
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 3$ The axiom of substitution: Exercise $3.2$
Category:Axiom of Replacement