P. 96 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zfreg 9501*	The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form". Axiom Reg of [BellMachover] p. 480. There is also a "strong form", not requiring that 𝐴 be a set, that can be proved with more difficulty (see zfregs 9641). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	elirrv 9502	The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. This is trivial to prove from zfregfr 9513 and efrirr 5604 (see elirrvALT 9514), but this proof is direct from ax-reg 9497. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9497 directly. (Revised by BTernaryTau, 27-Dec-2025.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirrvOLD 9503	Obsolete version of elirrv 9502 as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirr 9504	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ¬ 𝐴 ∈ 𝐴
Theorem	elneq 9505	A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	nelaneq 9506	A class is not an element of and equal to a class at the same time. Variant of elneq 9505 analogously to elnotel 9519 and en2lp 9515. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof shortened by TM, 31-Dec-2025.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	nelaneqOLD 9507	Obsolete version of nelaneq 9506 as of 31-Dec-2025. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	epinid0 9508	The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9506. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.)
⊢ ( E ∩ I ) = ∅
Theorem	sucprcreg 9509	A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.)
⊢ (¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴)
Theorem	ruv 9510	The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	ruALT 9511	Alternate proof of ru 3738, simplified using (indirectly) the Axiom of Regularity ax-reg 9497. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	disjcsn 9512	A class is disjoint from its singleton. A consequence of regularity. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 4-Apr-2019.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	zfregfr 9513	The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
⊢ E Fr 𝐴
Theorem	elirrvALT 9514	Alternate proof of elirrv 9502, shorter but using more axioms. (Contributed by BTernaryTau, 28-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	en2lp 9515	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)
Theorem	elnanel 9516	Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9515 and serves as an example in the context of Godel codes, see elnanelprv 35623. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴)
Theorem	cnvepnep 9517	The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9515. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.)
⊢ (◡ E ∩ E ) = ∅
Theorem	epnsym 9518	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ◡ E ≠ E
Theorem	elnotel 9519	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	elnel 9520	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴)
Theorem	en3lplem1 9521*	Lemma for en3lp 9523. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lplem2 9522*	Lemma for en3lp 9523. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lp 9523	No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 45081 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)
Theorem	preleqg 9524	Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9525. (Contributed by AV, 15-Jun-2022.)
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleq 9525	Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Revised by AV, 15-Jun-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleqALT 9526	Alternate proof of preleq 9525, not based on preleqg 9524: Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthreg 9527	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9497 (via the preleq 9525 step). See df-op 4587 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) (Proof shortened by AV, 15-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	suc11reg 9528	The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.)
⊢ (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)
Theorem	dford2 9529*	Assuming ax-reg 9497, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
2.5.2  Axiom of Infinity equivalents
Theorem	inf0 9530*	Existence of ω implies our axiom of infinity ax-inf 9547. The proof shows that the especially contrived class "ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) " exists, is a subset of its union, and contains a given set 𝑥 (and thus is nonempty). Thus, it provides an example demonstrating that a set 𝑦 exists with the necessary properties demanded by ax-inf 9547. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
⊢ (ω ∈ 𝑉 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
Theorem	inf1 9531	Variation of Axiom of Infinity (using zfinf 9548 as a hypothesis). Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 14-Oct-1996.) (Revised by David Abernethy, 1-Oct-2013.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	inf2 9532*	Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9548 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
Theorem	inf3lema 9533*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵))
Theorem	inf3lemb 9534*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	inf3lemc 9535*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴)))
Theorem	inf3lemd 9536*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥)
Theorem	inf3lem1 9537*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴))
Theorem	inf3lem2 9538*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥))
Theorem	inf3lem3 9539*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9501. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
Theorem	inf3lem4 9540*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴)))
Theorem	inf3lem5 9541*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴)))
Theorem	inf3lem6 9542*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥)
Theorem	inf3lem7 9543*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9544 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7901. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V)
Theorem	inf3 9544	Our Axiom of Infinity ax-inf 9547 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 9532, and the conclusion is the version of the Axiom of Infinity shown as Axiom 7 in [TakeutiZaring] p. 43. (Other standard versions are proved later as axinf2 9549 and zfinf2 9551.) The main proof is provided by inf3lema 9533 through inf3lem7 9543, and this final piece eliminates the auxiliary hypothesis of inf3lem7 9543. This proof is due to Ian Sutherland, Richard Heck, and Norman Megill and was posted on Usenet as shown below. Although the result is not new, the authors were unable to find a published proof. (As posted to sci.logic on 30-Oct-1996, with annotations added.) Theorem: The statement "There exists a nonempty set that is a subset of its union" implies the Axiom of Infinity. Proof: Let X be a nonempty set which is a subset of its union; the latter property is equivalent to saying that for any y in X, there exists a z in X such that y is in z. Define by finite recursion a function F:omega-->(power X) such that F_0 = 0 (See inf3lemb 9534.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9535.) Note: ^ means intersect, < means \in ("element of"). (Finite recursion as typically done requires the existence of omega; to avoid this we can just use transfinite recursion restricted to omega. F is a class-term that is not necessarily a set at this point.) Lemma 1. F_n subset F_n+1. (See inf3lem1 9537.) Proof: By induction: F_0 subset F_1. If y < F_n+1, then y^X subset F_n, so if F_n subset F_n+1, then y^X subset F_n+1, so y < F_n+2. Lemma 2. F_n =/= X. (See inf3lem2 9538.) Proof: By induction: F_0 =/= X because X is not empty. Assume F_n =/= X. Then there is a y in X that is not in F_n. By definition of X, there is a z in X that contains y. Suppose F_n+1 = X. Then z is in F_n+1, and z^X contains y, so z^X is not a subset of F_n, contrary to the definition of F_n+1. Lemma 3. F_n =/= F_n+1. (See inf3lem3 9539.) Proof: Using the identity y^X subset F_n <-> y^(X-F_n) = 0, we have F_n+1 = {y<X | y^(X-F_n) = 0}. Let q = {y<X-F_n | y^(X-F_n) = 0}. Then q subset F_n+1. Since X-F_n is not empty by Lemma 2 and q is the set of \in-minimal elements of X-F_n, by Foundation q is not empty, so q and therefore F_n+1 have an element not in F_n. Lemma 4. F_n proper_subset F_n+1. (See inf3lem4 9540.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9541.) Proof: Fix m and use induction on n > m. Basis: F_m proper_subset F_m+1 by Lemma 4. Induction: Assume F_m proper_subset F_n. Then since F_n proper_subset F_n+1, F_m proper_subset F_n+1 by transitivity of proper subset. By Lemma 5, F_m =/= F_n for m =/= n, so F is 1-1. (See inf3lem6 9542.) Thus, the inverse of F is a function with range omega and domain a subset of power X, so omega exists by Replacement. (See inf3lem7 9543.) Q.E.D. (Contributed by NM, 29-Oct-1996.)
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	infeq5i 9545	Half of infeq5 9546. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥)
Theorem	infeq5 9546	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex 9552.) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (∃𝑥 𝑥 ⊊ ∪ 𝑥 ↔ ω ∈ V)
2.6  ZF Set Theory - add the Axiom of Infinity
2.6.1  Introduce the Axiom of Infinity
Axiom	ax-inf 9547*	Axiom of Infinity. An axiom of Zermelo-Fraenkel set theory. This axiom is the gateway to "Cantor's paradise" (an expression coined by Hilbert). It asserts that given a starting set 𝑥, an infinite set 𝑦 built from it exists. Although our version is apparently not given in the literature, it is similar to, but slightly shorter than, the Axiom of Infinity in [FreydScedrov] p. 283 (see inf1 9531 and inf2 9532). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 9551 and omex 9552 and are based on the (nontrivial) proof of inf3 9544. This version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 9550. Theorem inf0 9530 shows the reverse derivation of our axiom from a standard one. Theorem inf5 9554 shows a very short way to state this axiom. The standard version of Infinity ax-inf2 9550 requires this axiom along with Regularity ax-reg 9497 for its derivation (as Theorem axinf2 9549 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9550 instead of this one. The derivation of this axiom from ax-inf2 9550 is shown by Theorem axinf 9553. Proofs should normally use the standard version ax-inf2 9550 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfinf 9548*	Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	axinf2 9549*	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 9547 and Regularity ax-reg 9497. This theorem should not be referenced in any proof. Instead, use ax-inf2 9550 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996.)
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Axiom	ax-inf2 9550*	A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 9551 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9549 above, using our version of Infinity ax-inf 9547 and the Axiom of Regularity ax-reg 9497. We will reference ax-inf2 9550 instead of axinf2 9549 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9547 from ax-inf2 9550 is shown by Theorem axinf 9553. (Contributed by NM, 3-Nov-1996.)
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	zfinf2 9551*	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9550 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2.6.2  Existence of omega (the set of natural numbers)
Theorem	omex 9552	The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. Remark 1.21 of [Schloeder] p. 3. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 9530. A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ¬ ω ∈ V; this would lead to ω = On by omon 7820 and Fin = V (the universe of all sets) by fineqv 9167. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 7831 through peano5 7835 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)
⊢ ω ∈ V
Theorem	axinf 9553*	The first version of the Axiom of Infinity ax-inf 9547 proved from the second version ax-inf2 9550. Note that we didn't use ax-reg 9497, unlike the other direction axinf2 9549. (Contributed by NM, 24-Apr-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	inf5 9554	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 9546). This provides us with a very compact way to express the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005.)
⊢ ∃𝑥 𝑥 ⊊ ∪ 𝑥
Theorem	omelon 9555	Omega is an ordinal number. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)
⊢ ω ∈ On
Theorem	dfom3 9556*	The class of natural numbers ω can be defined as the intersection of all inductive sets (which is the smallest inductive set, since inductive sets are closed under intersection), which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82. Definition 1.20 of [Schloeder] p. 3. (Contributed by NM, 6-Aug-1994.)
⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
Theorem	elom3 9557*	A simplification of elom 7811 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))
Theorem	dfom4 9558*	A simplification of df-om 7809 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom5 9559	ω is the smallest limit ordinal and can be defined as such (although the Axiom of Infinity is needed to ensure that at least one limit ordinal exists). Theorem 1.23 of [Schloeder] p. 4. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ ω = ∩ {𝑥 ∣ Lim 𝑥}
Theorem	oancom 9560	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60. (Contributed by NM, 10-Dec-2004.)
⊢ (1o +o ω) ≠ (ω +o 1o)
Theorem	isfinite 9561	A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011.)
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
Theorem	fict 9562	A finite set is countable (weaker version of isfinite 9561). (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω)
Theorem	nnsdom 9563	A natural number is strictly dominated by the set of natural numbers. Example 3 of [Enderton] p. 146. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐴 ∈ ω → 𝐴 ≺ ω)
Theorem	omenps 9564	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216. (Contributed by NM, 30-Jul-2003.)
⊢ ω ≈ (ω ∖ {∅})
Theorem	omensuc 9565	The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ω ≈ suc ω
Theorem	infdifsn 9566	Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ (ω ≼ 𝐴 → (𝐴 ∖ {𝐵}) ≈ 𝐴)
Theorem	infdiffi 9567	Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ Fin) → (𝐴 ∖ 𝐵) ≈ 𝐴)
Theorem	unbnn3 9568*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 9196 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	noinfep 9569*	Using the Axiom of Regularity in the form zfregfr 9513, show that there are no infinite descending ∈-chains. Proposition 7.34 of [TakeutiZaring] p. 44. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)
2.6.3  Cantor normal form
Syntax	ccnf 9570	Extend class notation with the Cantor normal form function.
class CNF
Definition	df-cnf 9571*	Define the Cantor normal form function, which takes as input a finitely supported function from 𝑦 to 𝑥 and outputs the corresponding member of the ordinal exponential 𝑥 ↑o 𝑦. The content of the original Cantor Normal Form theorem is that for 𝑥 = ω this function is a bijection onto ω ↑o 𝑦 for any ordinal 𝑦 (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to On). More can be said about the function, however, and in particular it is an order isomorphism for a certain easily defined well-ordering of the finitely supported functions, which gives an alternate definition cantnffval2 9604 of this function in terms of df-oi 9415. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑m 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)))
Theorem	cantnffval 9572*	The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)))
Theorem	cantnfdm 9573*	The domain of the Cantor normal form function (in later lemmas we will use dom (𝐴 CNF 𝐵) to abbreviate "the set of finitely supported functions from 𝐵 to 𝐴"). (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → dom (𝐴 CNF 𝐵) = 𝑆)
Theorem	cantnfvalf 9574*	Lemma for cantnf 9602. The function appearing in cantnfval 9577 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅)    ⇒   ⊢ 𝐹:ω⟶On
Theorem	cantnfs 9575	Elementhood in the set of finitely supported functions from 𝐵 to 𝐴. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
Theorem	cantnfcl 9576	Basic properties of the order isomorphism 𝐺 used later. The support of an 𝐹 ∈ 𝑆 is a finite subset of 𝐴, so it is well-ordered by E and the order isomorphism has domain a finite ordinal. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
Theorem	cantnfval 9577*	The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺))
Theorem	cantnfval2 9578*	Alternate expression for the value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺))
Theorem	cantnfsuc 9579*	The value of the recursive function 𝐻 at a successor. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ ω) → (𝐻‘suc 𝐾) = (((𝐴 ↑o (𝐺‘𝐾)) ·o (𝐹‘(𝐺‘𝐾))) +o (𝐻‘𝐾)))
Theorem	cantnfle 9580*	A lower bound on the CNF function. Since ((𝐴 CNF 𝐵)‘𝐹) is defined as the sum of (𝐴 ↑o 𝑥) ·o (𝐹‘𝑥) over all 𝑥 in the support of 𝐹, it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all 𝐶 ∈ 𝐵 instead of just those 𝐶 in the support). (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 28-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
Theorem	cantnflt 9581*	An upper bound on the partial sums of the CNF function. Since each term dominates all previous terms, by induction we can bound the whole sum with any exponent 𝐴 ↑o 𝐶 where 𝐶 is larger than any exponent (𝐺‘𝑥), 𝑥 ∈ 𝐾 which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ suc dom 𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → (𝐺 “ 𝐾) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑o 𝐶))
Theorem	cantnflt2 9582	An upper bound on the CNF function. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))
Theorem	cantnff 9583	The CNF function is a function from finitely supported functions from 𝐵 to 𝐴, to the ordinal exponential 𝐴 ↑o 𝐵. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵))
Theorem	cantnf0 9584	The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
Theorem	cantnfrescl 9585*	A function is finitely supported from 𝐵 to 𝐴 iff the extended function is finitely supported from 𝐷 to 𝐴. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ 𝑇 = dom (𝐴 CNF 𝐷)    ⇒   ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇))
Theorem	cantnfres 9586*	The CNF function respects extensions of the domain to a larger ordinal. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    &   ⊢ 𝑇 = dom (𝐴 CNF 𝐷)    &   ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋)))
Theorem	cantnfp1lem1 9587*	Lemma for cantnfp1 9590. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑆)
Theorem	cantnfp1lem2 9588*	Lemma for cantnfp1 9590. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    &   ⊢ (𝜑 → ∅ ∈ 𝑌)    &   ⊢ 𝑂 = OrdIso( E , (𝐹 supp ∅))    ⇒   ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂)
Theorem	cantnfp1lem3 9589*	Lemma for cantnfp1 9590. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    &   ⊢ (𝜑 → ∅ ∈ 𝑌)    &   ⊢ 𝑂 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐹‘(𝑂‘𝑘))) +o 𝑧)), ∅)    &   ⊢ 𝐾 = OrdIso( E , (𝐺 supp ∅))    &   ⊢ 𝑀 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐾‘𝑘)) ·o (𝐺‘(𝐾‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
Theorem	cantnfp1 9590*	If 𝐹 is created by adding a single term (𝐹‘𝑋) = 𝑌 to 𝐺, where 𝑋 is larger than any element of the support of 𝐺, then 𝐹 is also a finitely supported function and it is assigned the value ((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑧 where 𝑧 is the value of 𝐺. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))))
Theorem	oemapso 9591*	The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9458). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑆)
Theorem	oemapval 9592*	Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))))
Theorem	oemapvali 9593*	If 𝐹 < 𝐺, then there is some 𝑧 witnessing this, but we can say more and in fact there is a definable expression 𝑋 that also witnesses 𝐹 < 𝐺. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
Theorem	cantnflem1a 9594*	Lemma for cantnf 9602. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
Theorem	cantnflem1b 9595*	Lemma for cantnf 9602. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢))
Theorem	cantnflem1c 9596*	Lemma for cantnf 9602. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) (Proof shortened by AV, 4-Apr-2020.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
Theorem	cantnflem1d 9597*	Lemma for cantnf 9602. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐺‘(𝑂‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
Theorem	cantnflem1 9598*	Lemma for cantnf 9602. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation 𝑇 is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct 𝐹, 𝐺 are 𝑇 -related as 𝐹 < 𝐺 or 𝐺 < 𝐹, and WLOG assuming that 𝐹 < 𝐺, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐺‘(𝑂‘𝑘))) +o 𝑧)), ∅)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Theorem	cantnflem2 9599*	Lemma for cantnf 9602. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
Theorem	cantnflem3 9600*	Lemma for cantnf 9602. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than 𝐶 has a normal form, we can use oeeu 8531 to factor 𝐶 into the form ((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍 where 0 < 𝑌 < 𝐴 and 𝑍 < (𝐴 ↑o 𝑋) (and a fortiori 𝑋 < 𝐵). Then since 𝑍 < (𝐴 ↑o 𝑋) ≤ (𝐴 ↑o 𝑋) ·o 𝑌 ≤ 𝐶, 𝑍 has a normal form, and by appending the term (𝐴 ↑o 𝑋) ·o 𝑌 using cantnfp1 9590 we get a normal form for 𝐶. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    &   ⊢ 𝑋 = ∪ ∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑o 𝑐)}    &   ⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴 ↑o 𝑋) ·o 𝑎) +o 𝑏) = 𝐶))    &   ⊢ 𝑌 = (1st ‘𝑃)    &   ⊢ 𝑍 = (2nd ‘𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵))