P. 97 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	epinid0 9601	The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9600. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.)
⊢ ( E ∩ I ) = ∅
Theorem	sucprcreg 9602	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 9603	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 9604	Alternate proof of ru 3776, simplified using (indirectly) the Axiom of Regularity ax-reg 9593. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	disjcsn 9605	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 9606	The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
⊢ E Fr 𝐴
Theorem	en2lp 9607	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 9608	Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9607 and serves as an example in the context of Godel codes, see elnanelprv 34886. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴)
Theorem	cnvepnep 9609	The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9607. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.)
⊢ (◡ E ∩ E ) = ∅
Theorem	epnsym 9610	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ◡ E ≠ E
Theorem	elnotel 9611	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	elnel 9612	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴)
Theorem	en3lplem1 9613*	Lemma for en3lp 9615. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lplem2 9614*	Lemma for en3lp 9615. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lp 9615	No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 44072 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)
Theorem	preleqg 9616	Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9617. (Contributed by AV, 15-Jun-2022.)
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleq 9617	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 9618	Alternate proof of preleq 9617, not based on preleqg 9616: 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 9619	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9593 (via the preleq 9617 step). See df-op 4635 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 9620	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 9621*	Assuming ax-reg 9593, 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 9622*	Existence of ω implies our axiom of infinity ax-inf 9639. 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 9639. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
⊢ (ω ∈ 𝑉 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
Theorem	inf1 9623	Variation of Axiom of Infinity (using zfinf 9640 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 9624*	Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9640 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
Theorem	inf3lema 9625*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵))
Theorem	inf3lemb 9626*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	inf3lemc 9627*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴)))
Theorem	inf3lemd 9628*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥)
Theorem	inf3lem1 9629*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴))
Theorem	inf3lem2 9630*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥))
Theorem	inf3lem3 9631*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9596. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
Theorem	inf3lem4 9632*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴)))
Theorem	inf3lem5 9633*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴)))
Theorem	inf3lem6 9634*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥)
Theorem	inf3lem7 9635*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9636 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7947. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V)
Theorem	inf3 9636	Our Axiom of Infinity ax-inf 9639 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 9624, 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 9641 and zfinf2 9643.) The main proof is provided by inf3lema 9625 through inf3lem7 9635, and this final piece eliminates the auxiliary hypothesis of inf3lem7 9635. 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 9626.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9627.) 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 9629.) 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 9630.) 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 9631.) 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 9632.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9633.) 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 9634.) 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 9635.) Q.E.D. (Contributed by NM, 29-Oct-1996.)
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	infeq5i 9637	Half of infeq5 9638. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥)
Theorem	infeq5 9638	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 9644.) 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 9639*	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 9623 and inf2 9624). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 9643 and omex 9644 and are based on the (nontrivial) proof of inf3 9636. This version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 9642. Theorem inf0 9622 shows the reverse derivation of our axiom from a standard one. Theorem inf5 9646 shows a very short way to state this axiom. The standard version of Infinity ax-inf2 9642 requires this axiom along with Regularity ax-reg 9593 for its derivation (as Theorem axinf2 9641 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9642 instead of this one. The derivation of this axiom from ax-inf2 9642 is shown by Theorem axinf 9645. Proofs should normally use the standard version ax-inf2 9642 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfinf 9640*	Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	axinf2 9641*	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 9639 and Regularity ax-reg 9593. This theorem should not be referenced in any proof. Instead, use ax-inf2 9642 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 9642*	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 9643 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9641 above, using our version of Infinity ax-inf 9639 and the Axiom of Regularity ax-reg 9593. We will reference ax-inf2 9642 instead of axinf2 9641 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9639 from ax-inf2 9642 is shown by Theorem axinf 9645. (Contributed by NM, 3-Nov-1996.)
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	zfinf2 9643*	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9642 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2.6.2  Existence of omega (the set of natural numbers)
Theorem	omex 9644	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 9622. 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 7871 and Fin = V (the universe of all sets) by fineqv 9269. 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 7883 through peano5 7888 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)
⊢ ω ∈ V
Theorem	axinf 9645*	The first version of the Axiom of Infinity ax-inf 9639 proved from the second version ax-inf2 9642. Note that we didn't use ax-reg 9593, unlike the other direction axinf2 9641. (Contributed by NM, 24-Apr-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	inf5 9646	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 9638). 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 9647	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 9648*	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 9649*	A simplification of elom 7862 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))
Theorem	dfom4 9650*	A simplification of df-om 7860 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom5 9651	ω 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 9652	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 9653	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 9654	A finite set is countable (weaker version of isfinite 9653). (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω)
Theorem	nnsdom 9655	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 9656	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 9657	The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ω ≈ suc ω
Theorem	infdifsn 9658	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 9659	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 9660*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 9305 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	noinfep 9661*	Using the Axiom of Regularity in the form zfregfr 9606, 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 9662	Extend class notation with the Cantor normal form function.
class CNF
Definition	df-cnf 9663*	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 9696 of this function in terms of df-oi 9511. (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 9664*	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 9665*	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 9666*	Lemma for cantnf 9694. The function appearing in cantnfval 9669 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅)    ⇒   ⊢ 𝐹:ω⟶On
Theorem	cantnfs 9667	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 9668	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 9669*	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 9670*	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 9671*	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 9672*	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 9673*	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 9674	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 9675	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 9676	The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
Theorem	cantnfrescl 9677*	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 9678*	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 9679*	Lemma for cantnfp1 9682. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑆)
Theorem	cantnfp1lem2 9680*	Lemma for cantnfp1 9682. (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 9681*	Lemma for cantnfp1 9682. (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 9682*	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 9683*	The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9554). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑆)
Theorem	oemapval 9684*	Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))))
Theorem	oemapvali 9685*	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 9686*	Lemma for cantnf 9694. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
Theorem	cantnflem1b 9687*	Lemma for cantnf 9694. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢))
Theorem	cantnflem1c 9688*	Lemma for cantnf 9694. (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 9689*	Lemma for cantnf 9694. (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 9690*	Lemma for cantnf 9694. 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 9691*	Lemma for cantnf 9694. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
Theorem	cantnflem3 9692*	Lemma for cantnf 9694. 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 8609 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 9682 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 𝐵))
Theorem	cantnflem4 9693*	Lemma for cantnf 9694. Complete the induction step of cantnflem3 9692. (Contributed by Mario Carneiro, 25-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    &   ⊢ 𝑋 = ∪ ∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑o 𝑐)}    &   ⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴 ↑o 𝑋) ·o 𝑎) +o 𝑏) = 𝐶))    &   ⊢ 𝑌 = (1st ‘𝑃)    &   ⊢ 𝑍 = (2nd ‘𝑃)    ⇒   ⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵))
Theorem	cantnf 9694*	The Cantor Normal Form theorem. The function (𝐴 CNF 𝐵), which maps a finitely supported function from 𝐵 to 𝐴 to the sum ((𝐴 ↑o 𝑓(𝑎1)) ∘ 𝑎1) +o ((𝐴 ↑o 𝑓(𝑎2)) ∘ 𝑎2) +o ... over all indices 𝑎 < 𝐵 such that 𝑓(𝑎) is nonzero, is an order isomorphism from the ordering 𝑇 of finitely supported functions to the set (𝐴 ↑o 𝐵) under the natural order. Setting 𝐴 = ω and letting 𝐵 be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres 9678, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵)))
Theorem	oemapwe 9695*	The lexicographic order on a function space of ordinals gives a well-ordering with order type equal to the ordinal exponential. This provides an alternate definition of the ordinal exponential. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝑇 We 𝑆 ∧ dom OrdIso(𝑇, 𝑆) = (𝐴 ↑o 𝐵)))
Theorem	cantnffval2 9696*	An alternate definition of df-cnf 9663 which relies on cantnf 9694. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9665 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆))
Theorem	cantnff1o 9697	Simplify the isomorphism of cantnf 9694 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵))
Theorem	wemapwe 9698*	Construct lexicographic order on a function space based on a reverse well-ordering of the indices and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by AV, 3-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑆 We 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ 𝐹 = OrdIso(𝑅, 𝐴)    &   ⊢ 𝐺 = OrdIso(𝑆, 𝐵)    &   ⊢ 𝑍 = (𝐺‘∅)    ⇒   ⊢ (𝜑 → 𝑇 We 𝑈)
Theorem	oef1o 9699*	A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7304.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ (On ∖ 1o))    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺)))    &   ⊢ 𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵))    ⇒   ⊢ (𝜑 → 𝐻:(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷))
Theorem	cnfcomlem 9700*	Lemma for cnfcom 9701. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)
⊢ 𝑆 = dom (ω CNF 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))    &   ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)    &   ⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)    &   ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))    &   ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))    &   ⊢ (𝜑 → 𝐼 ∈ dom 𝐺)    &   ⊢ (𝜑 → 𝑂 ∈ (ω ↑o (𝐺‘𝐼)))    &   ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂)    ⇒   ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))