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	zfregfr 9501	The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
⊢ E Fr 𝐴
Theorem	elirrvALT 9502	Alternate proof of elirrv 9490, shorter but using more axioms. (Contributed by BTernaryTau, 28-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	en2lp 9503	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 9504	Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9503 and serves as an example in the context of Godel codes, see elnanelprv 35494. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴)
Theorem	cnvepnep 9505	The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9503. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.)
⊢ (◡ E ∩ E ) = ∅
Theorem	epnsym 9506	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ◡ E ≠ E
Theorem	elnotel 9507	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	elnel 9508	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴)
Theorem	en3lplem1 9509*	Lemma for en3lp 9511. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lplem2 9510*	Lemma for en3lp 9511. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lp 9511	No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 44961 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)
Theorem	preleqg 9512	Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9513. (Contributed by AV, 15-Jun-2022.)
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleq 9513	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 9514	Alternate proof of preleq 9513, not based on preleqg 9512: 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 9515	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9485 (via the preleq 9513 step). See df-op 4582 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 9516	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 9517*	Assuming ax-reg 9485, 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 9518*	Existence of ω implies our axiom of infinity ax-inf 9535. 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 9535. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
⊢ (ω ∈ 𝑉 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
Theorem	inf1 9519	Variation of Axiom of Infinity (using zfinf 9536 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 9520*	Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9536 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
Theorem	inf3lema 9521*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵))
Theorem	inf3lemb 9522*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	inf3lemc 9523*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴)))
Theorem	inf3lemd 9524*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥)
Theorem	inf3lem1 9525*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴))
Theorem	inf3lem2 9526*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥))
Theorem	inf3lem3 9527*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9489. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))
Theorem	inf3lem4 9528*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴)))
Theorem	inf3lem5 9529*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴)))
Theorem	inf3lem6 9530*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥)
Theorem	inf3lem7 9531*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9532 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7895. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V)
Theorem	inf3 9532	Our Axiom of Infinity ax-inf 9535 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 9520, 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 9537 and zfinf2 9539.) The main proof is provided by inf3lema 9521 through inf3lem7 9531, and this final piece eliminates the auxiliary hypothesis of inf3lem7 9531. 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 9522.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9523.) 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 9525.) 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 9526.) 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 9527.) 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 9528.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9529.) 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 9530.) 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 9531.) Q.E.D. (Contributed by NM, 29-Oct-1996.)
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	infeq5i 9533	Half of infeq5 9534. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥)
Theorem	infeq5 9534	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 9540.) 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 9535*	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 9519 and inf2 9520). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 9539 and omex 9540 and are based on the (nontrivial) proof of inf3 9532. This version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 9538. Theorem inf0 9518 shows the reverse derivation of our axiom from a standard one. Theorem inf5 9542 shows a very short way to state this axiom. The standard version of Infinity ax-inf2 9538 requires this axiom along with Regularity ax-reg 9485 for its derivation (as Theorem axinf2 9537 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9538 instead of this one. The derivation of this axiom from ax-inf2 9538 is shown by Theorem axinf 9541. Proofs should normally use the standard version ax-inf2 9538 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfinf 9536*	Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	axinf2 9537*	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 9535 and Regularity ax-reg 9485. This theorem should not be referenced in any proof. Instead, use ax-inf2 9538 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 9538*	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 9539 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9537 above, using our version of Infinity ax-inf 9535 and the Axiom of Regularity ax-reg 9485. We will reference ax-inf2 9538 instead of axinf2 9537 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9535 from ax-inf2 9538 is shown by Theorem axinf 9541. (Contributed by NM, 3-Nov-1996.)
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	zfinf2 9539*	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9538 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2.6.2  Existence of omega (the set of natural numbers)
Theorem	omex 9540	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 9518. 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 7814 and Fin = V (the universe of all sets) by fineqv 9158. 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 7825 through peano5 7829 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)
⊢ ω ∈ V
Theorem	axinf 9541*	The first version of the Axiom of Infinity ax-inf 9535 proved from the second version ax-inf2 9538. Note that we didn't use ax-reg 9485, unlike the other direction axinf2 9537. (Contributed by NM, 24-Apr-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	inf5 9542	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 9534). 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 9543	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 9544*	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 9545*	A simplification of elom 7805 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))
Theorem	dfom4 9546*	A simplification of df-om 7803 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom5 9547	ω 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 9548	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 9549	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 9550	A finite set is countable (weaker version of isfinite 9549). (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω)
Theorem	nnsdom 9551	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 9552	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 9553	The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ω ≈ suc ω
Theorem	infdifsn 9554	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 9555	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 9556*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 9187 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	noinfep 9557*	Using the Axiom of Regularity in the form zfregfr 9501, 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 9558	Extend class notation with the Cantor normal form function.
class CNF
Definition	df-cnf 9559*	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 9592 of this function in terms of df-oi 9403. (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 9560*	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 9561*	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 9562*	Lemma for cantnf 9590. The function appearing in cantnfval 9565 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅)    ⇒   ⊢ 𝐹:ω⟶On
Theorem	cantnfs 9563	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 9564	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 9565*	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 9566*	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 9567*	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 9568*	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 9569*	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 9570	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 9571	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 9572	The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
Theorem	cantnfrescl 9573*	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 9574*	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 9575*	Lemma for cantnfp1 9578. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑆)
Theorem	cantnfp1lem2 9576*	Lemma for cantnfp1 9578. (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 9577*	Lemma for cantnfp1 9578. (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 9578*	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 9579*	The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9446). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑆)
Theorem	oemapval 9580*	Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))))
Theorem	oemapvali 9581*	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 9582*	Lemma for cantnf 9590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
Theorem	cantnflem1b 9583*	Lemma for cantnf 9590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢))
Theorem	cantnflem1c 9584*	Lemma for cantnf 9590. (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 9585*	Lemma for cantnf 9590. (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 9586*	Lemma for cantnf 9590. 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 9587*	Lemma for cantnf 9590. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
Theorem	cantnflem3 9588*	Lemma for cantnf 9590. 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 8524 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 9578 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 9589*	Lemma for cantnf 9590. Complete the induction step of cantnflem3 9588. (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 9590*	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 9574, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵)))
Theorem	oemapwe 9591*	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 9592*	An alternate definition of df-cnf 9559 which relies on cantnf 9590. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9561 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆))
Theorem	cantnff1o 9593	Simplify the isomorphism of cantnf 9590 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵))
Theorem	wemapwe 9594*	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 9595*	A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7242.) (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 9596*	Lemma for cnfcom 9597. (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 (𝐹‘(𝐺‘𝐼))))
Theorem	cnfcom 9597*	Any ordinal 𝐵 is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (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 𝐺)    ⇒   ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))
Theorem	cnfcom2lem 9598*	Lemma for cnfcom2 9599. (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 𝐺)    &   ⊢ (𝜑 → ∅ ∈ 𝐵)    ⇒   ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
Theorem	cnfcom2 9599*	Any nonzero ordinal 𝐵 is equinumerous to the leading term of its Cantor normal form. (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 𝐺)    &   ⊢ (𝜑 → ∅ ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)))
Theorem	cnfcom3lem 9600*	Lemma for cnfcom3 9601. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)
⊢ 𝑆 = dom (ω CNF 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))    &   ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)    &   ⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)    &   ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))    &   ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))    &   ⊢ 𝑊 = (𝐺‘∪ dom 𝐺)    &   ⊢ (𝜑 → ω ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))