P. 95 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inf3lem7 9401*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9402 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7808. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V)
Theorem	inf3 9402	Our Axiom of Infinity ax-inf 9405 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 9390, 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 9407 and zfinf2 9409.) The main proof is provided by inf3lema 9391 through inf3lem7 9401, and this final piece eliminates the auxiliary hypothesis of inf3lem7 9401. 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 9392.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9393.) 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 9395.) 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 9396.) 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 9397.) 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 9398.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9399.) 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 9400.) 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 9401.) Q.E.D. (Contributed by NM, 29-Oct-1996.)
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	infeq5i 9403	Half of infeq5 9404. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥)
Theorem	infeq5 9404	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 9410.) 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 9405*	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 9389 and inf2 9390). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 9409 and omex 9410 and are based on the (nontrivial) proof of inf3 9402. This version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 9408. Theorem inf0 9388 shows the reverse derivation of our axiom from a standard one. Theorem inf5 9412 shows a very short way to state this axiom. The standard version of Infinity ax-inf2 9408 requires this axiom along with Regularity ax-reg 9360 for its derivation (as Theorem axinf2 9407 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9408 instead of this one. The derivation of this axiom from ax-inf2 9408 is shown by Theorem axinf 9411. Proofs should normally use the standard version ax-inf2 9408 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfinf 9406*	Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	axinf2 9407*	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 9405 and Regularity ax-reg 9360. This theorem should not be referenced in any proof. Instead, use ax-inf2 9408 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 9408*	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 9409 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9407 above, using our version of Infinity ax-inf 9405 and the Axiom of Regularity ax-reg 9360. We will reference ax-inf2 9408 instead of axinf2 9407 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9405 from ax-inf2 9408 is shown by Theorem axinf 9411. (Contributed by NM, 3-Nov-1996.)
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	zfinf2 9409*	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9408 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)
2.6.2  Existence of omega (the set of natural numbers)
Theorem	omex 9410	The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 9388. 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 7733 and Fin = V (the universe of all sets) by fineqv 9047. 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 7744 through peano5 7749 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.)
⊢ ω ∈ V
Theorem	axinf 9411*	The first version of the Axiom of Infinity ax-inf 9405 proved from the second version ax-inf2 9408. Note that we didn't use ax-reg 9360, unlike the other direction axinf2 9407. (Contributed by NM, 24-Apr-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	inf5 9412	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 9404). 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 9413	Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)
⊢ ω ∈ On
Theorem	dfom3 9414*	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. (Contributed by NM, 6-Aug-1994.)
⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
Theorem	elom3 9415*	A simplification of elom 7724 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥))
Theorem	dfom4 9416*	A simplification of df-om 7722 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.)
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom5 9417	ω 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). (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ ω = ∩ {𝑥 ∣ Lim 𝑥}
Theorem	oancom 9418	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 9419	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 9420	A finite set is countable (weaker version of isfinite 9419). (Contributed by Thierry Arnoux, 27-Mar-2018.)
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω)
Theorem	nnsdom 9421	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 9422	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 9423	The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ω ≈ suc ω
Theorem	infdifsn 9424	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 9425	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 9426*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 9079 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	noinfep 9427*	Using the Axiom of Regularity in the form zfregfr 9372, 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 9428	Extend class notation with the Cantor normal form function.
class CNF
Definition	df-cnf 9429*	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 9462 of this function in terms of df-oi 9278. (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 9430*	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 9431*	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 9432*	Lemma for cantnf 9460. The function appearing in cantnfval 9435 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅)    ⇒   ⊢ 𝐹:ω⟶On
Theorem	cantnfs 9433	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 9434	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 9435*	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 9436*	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 9437*	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 9438*	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 9439*	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 9440	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 9441	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 9442	The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
Theorem	cantnfrescl 9443*	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 9444*	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 9445*	Lemma for cantnfp1 9448. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑆)
Theorem	cantnfp1lem2 9446*	Lemma for cantnfp1 9448. (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 9447*	Lemma for cantnfp1 9448. (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 9448*	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 9449*	The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9321). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑆)
Theorem	oemapval 9450*	Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))))
Theorem	oemapvali 9451*	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 9452*	Lemma for cantnf 9460. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
Theorem	cantnflem1b 9453*	Lemma for cantnf 9460. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢))
Theorem	cantnflem1c 9454*	Lemma for cantnf 9460. (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 9455*	Lemma for cantnf 9460. (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 9456*	Lemma for cantnf 9460. 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 9457*	Lemma for cantnf 9460. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
Theorem	cantnflem3 9458*	Lemma for cantnf 9460. 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 8443 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 9448 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 9459*	Lemma for cantnf 9460. Complete the induction step of cantnflem3 9458. (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 9460*	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 9444, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵)))
Theorem	oemapwe 9461*	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 9462*	An alternate definition of df-cnf 9429 which relies on cantnf 9460. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9431 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆))
Theorem	cantnff1o 9463	Simplify the isomorphism of cantnf 9460 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵))
Theorem	wemapwe 9464*	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 9465*	A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7184.) (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 9466*	Lemma for cnfcom 9467. (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 9467*	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 9468*	Lemma for cnfcom2 9469. (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 9469*	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 9470*	Lemma for cnfcom3 9471. (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))
Theorem	cnfcom3 9471*	Any infinite ordinal 𝐵 is equinumerous to a power of ω. (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c 9473.) (Contributed by Mario Carneiro, 28-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 𝐺)    &   ⊢ (𝜑 → ω ⊆ 𝐵)    &   ⊢ 𝑋 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹‘𝑊) ·o 𝑣) +o 𝑢))    &   ⊢ 𝑌 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))    &   ⊢ 𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺))    ⇒   ⊢ (𝜑 → 𝑁:𝐵–1-1-onto→(ω ↑o 𝑊))
Theorem	cnfcom3clem 9472*	Lemma for cnfcom3c 9473. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)
⊢ 𝑆 = dom (ω CNF 𝐴)    &   ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝑏)    &   ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))    &   ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)    &   ⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)    &   ⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))    &   ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))    &   ⊢ 𝑊 = (𝐺‘∪ dom 𝐺)    &   ⊢ 𝑋 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹‘𝑊) ·o 𝑣) +o 𝑢))    &   ⊢ 𝑌 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))    &   ⊢ 𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺))    &   ⊢ 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁)    ⇒   ⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))
Theorem	cnfcom3c 9473*	Wrap the construction of cnfcom3 9471 into an existential quantifier. For any ω ⊆ 𝑏, there is a bijection from 𝑏 to some power of ω. Furthermore, this bijection is canonical , which means that we can find a single function 𝑔 which will give such bijections for every 𝑏 less than some arbitrarily large bound 𝐴. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))
2.6.4  Transitive closure of a relation
Syntax	cttrcl 9474	Declare the syntax for the transitive closure of a class.
class t++𝑅
Definition	df-ttrcl 9475*	Define the transitive closure of a class. This is the smallest relationship containing 𝑅 (or more precisely, the relation (𝑅 ↾ V) induced by 𝑅) and having the transitive property. Definition from [Levy] p. 59, who denotes it as 𝑅∗ and calls it the "ancestral" of 𝑅. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
Theorem	ttrcleq 9476	Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝑅 = 𝑆 → t++𝑅 = t++𝑆)
Theorem	nfttrcld 9477	Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ (𝜑 → Ⅎ𝑥𝑅)    ⇒   ⊢ (𝜑 → Ⅎ𝑥t++𝑅)
Theorem	nfttrcl 9478	Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥t++𝑅
Theorem	relttrcl 9479	The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Rel t++𝑅
Theorem	brttrcl 9480*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘𝑛) = 𝐵) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
Theorem	brttrcl2 9481*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 24-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘suc 𝑛) = 𝐵) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
Theorem	ssttrcl 9482	If 𝑅 is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)
Theorem	ttrcltr 9483	The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅
Theorem	ttrclresv 9484	The transitive closure of 𝑅 restricted to V is the same as the transitive closure of 𝑅 itself. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ t++(𝑅 ↾ V) = t++𝑅
Theorem	ttrclco 9485	Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ (t++𝑅 ∘ 𝑅) ⊆ t++𝑅
Theorem	cottrcl 9486	Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ (𝑅 ∘ t++𝑅) ⊆ t++𝑅
Theorem	ttrclss 9487	If 𝑅 is a subclass of 𝑆 and 𝑆 is transitive, then the transitive closure of 𝑅 is a subclass of 𝑆. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)
Theorem	dmttrcl 9488	The domain of a transitive closure is the same as the domain of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ dom t++𝑅 = dom 𝑅
Theorem	rnttrcl 9489	The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ ran t++𝑅 = ran 𝑅
Theorem	ttrclexg 9490	If 𝑅 is a set, then so is t++𝑅. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ (𝑅 ∈ 𝑉 → t++𝑅 ∈ V)
Theorem	dfttrcl2 9491*	When 𝑅 is a set and a relationship, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → t++𝑅 = ∩ {𝑧 ∣ (𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
Theorem	ttrclselem1 9492*	Lemma for ttrclse 9494. Show that all finite ordinal function values of 𝐹 are subsets of 𝐴. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))    ⇒   ⊢ (𝑁 ∈ ω → (𝐹‘𝑁) ⊆ 𝐴)
Theorem	ttrclselem2 9493*	Lemma for ttrclse 9494. Show that a suc 𝑁 element long chain gives membership in the 𝑁-th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))
Theorem	ttrclse 9494	If 𝑅 is set-like over 𝐴, then the transitive closure of the restriction of 𝑅 to 𝐴 is set-like over 𝐴. This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ (𝑅 Se 𝐴 → t++(𝑅 ↾ 𝐴) Se 𝐴)
2.6.5  Transitive closure
Theorem	trcl 9495*	For any set 𝐴, show the properties of its transitive closure 𝐶. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 9496 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ (𝑧 ∪ ∪ 𝑧)), 𝐴) ↾ ω)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ ω (𝐹‘𝑦)    ⇒   ⊢ (𝐴 ⊆ 𝐶 ∧ Tr 𝐶 ∧ ∀𝑥((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) → 𝐶 ⊆ 𝑥))
Theorem	tz9.1 9496*	Every set has a transitive closure (the smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 9495 for an explicit expression for the transitive closure. Apparently open problems are whether this theorem can be proved without the Axiom of Infinity; if not, then whether it implies Infinity; and if not, what is the "property" that Infinity has that the other axioms don't have that is weaker than Infinity itself? (Added 22-Mar-2011) The following article seems to answer the first question, that it can't be proved without Infinity, in the affirmative: Mancini, Antonella and Zambella, Domenico (2001). "A note on recursive models of set theories." Notre Dame Journal of Formal Logic, 42(2):109-115. (Thanks to Scott Fenton.) (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	tz9.1c 9497*	Alternate expression for the existence of transitive closures tz9.1 9496: the intersection of all transitive sets containing 𝐴 is a set. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	epfrs 9498*	The strong form of the Axiom of Regularity (no sethood requirement on 𝐴), with the axiom itself present as an antecedent. See also zfregs 9499. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ (( E Fr 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs 9499*	The strong form of the Axiom of Regularity, which does not require that 𝐴 be a set. Axiom 6' of [TakeutiZaring] p. 21. See also epfrs 9498. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs2 9500*	Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))