P. 93 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cantnfvalf 9201*	Lemma for cantnf 9229. The function appearing in cantnfval 9204 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅)    ⇒   ⊢ 𝐹:ω⟶On
Theorem	cantnfs 9202	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 9203	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 9204*	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 9205*	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 9206*	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 9207*	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 9208*	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 9209	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 9210	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 9211	The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → ∅ ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
Theorem	cantnfrescl 9212*	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 9213*	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 9214*	Lemma for cantnfp1 9217. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)    &   ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑆)
Theorem	cantnfp1lem2 9215*	Lemma for cantnfp1 9217. (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 9216*	Lemma for cantnfp1 9217. (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 9217*	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 9218*	The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9090). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑆)
Theorem	oemapval 9219*	Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))))
Theorem	oemapvali 9220*	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 9221*	Lemma for cantnf 9229. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
Theorem	cantnflem1b 9222*	Lemma for cantnf 9229. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹𝑇𝐺)    &   ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}    &   ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))    ⇒   ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢))
Theorem	cantnflem1c 9223*	Lemma for cantnf 9229. (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 9224*	Lemma for cantnf 9229. (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 9225*	Lemma for cantnf 9229. 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 9226*	Lemma for cantnf 9229. (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
Theorem	cantnflem3 9227*	Lemma for cantnf 9229. 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 8260 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 9217 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 9228*	Lemma for cantnf 9229. Complete the induction step of cantnflem3 9227. (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 9229*	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 9213, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵)))
Theorem	oemapwe 9230*	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 9231*	An alternate definition of df-cnf 9198 which relies on cantnf 9229. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9200 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆))
Theorem	cantnff1o 9232	Simplify the isomorphism of cantnf 9229 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝑆 = dom (𝐴 CNF 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵))
Theorem	wemapwe 9233*	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 9234*	A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7070.) (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 9235*	Lemma for cnfcom 9236. (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 9236*	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 9237*	Lemma for cnfcom2 9238. (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 9238*	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 9239*	Lemma for cnfcom3 9240. (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 9240*	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 9242.) (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 9241*	Lemma for cnfcom3c 9242. (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 9242*	Wrap the construction of cnfcom3 9240 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
Theorem	trcl 9243*	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 9244 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 9244*	Every set has a transitive closure (the smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 9243 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 9245*	Alternate expression for the existence of transitive closures tz9.1 9244: the intersection of all transitive sets containing 𝐴 is a set. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	epfrs 9246*	The strong form of the Axiom of Regularity (no sethood requirement on 𝐴), with the axiom itself present as an antecedent. See also zfregs 9247. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ (( E Fr 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs 9247*	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 9246. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs2 9248*	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.)
⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
Theorem	setind 9249*	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setind2 9250	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996). (Contributed by NM, 17-Sep-2003.)
⊢ (𝒫 𝐴 ⊆ 𝐴 → 𝐴 = V)
Syntax	ctc 9251	Extend class notation to include the transitive closure function.
class TC
Definition	df-tc 9252*	The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
Theorem	tcvalg 9253*	Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 9174; see tz9.1 9244.) (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
Theorem	tcid 9254	Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (TC‘𝐴))
Theorem	tctr 9255	Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ Tr (TC‘𝐴)
Theorem	tcmin 9256	Defining property of the transitive closure function: it is a subset of any transitive class containing 𝐴. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → (TC‘𝐴) ⊆ 𝐵))
Theorem	tc2 9257*	A variant of the definition of the transitive closure function, using instead the smallest transitive set containing 𝐴 as a member, gives almost the same set, except that 𝐴 itself must be added because it is not usually a member of (TC‘𝐴) (and it is never a member if 𝐴 is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((TC‘𝐴) ∪ {𝐴}) = ∩ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)}
Theorem	tcsni 9258	The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (TC‘{𝐴}) = ((TC‘𝐴) ∪ {𝐴})
Theorem	tcss 9259	The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ⊆ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴))
Theorem	tcel 9260	The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴))
Theorem	tcidm 9261	The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (TC‘(TC‘𝐴)) = (TC‘𝐴)
Theorem	tc0 9262	The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (TC‘∅) = ∅
Theorem	tc00 9263	The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅))
2.6.5  Rank
Syntax	cr1 9264	Extend class definition to include the cumulative hierarchy of sets function.
class 𝑅1
Syntax	crnk 9265	Extend class definition to include rank function.
class rank
Definition	df-r1 9266	Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 9293). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as Theorems r10 9270, r1suc 9272, and r1lim 9274. Theorem r1val1 9288 shows a recursive definition that works for all values, and Theorems r1val2 9339 and r1val3 9340 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95). (Contributed by NM, 2-Sep-2003.)
⊢ 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
Definition	df-rank 9267*	Define the rank function. See rankval 9318, rankval2 9320, rankval3 9342, or rankval4 9369 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 9335 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9338. (Contributed by NM, 11-Oct-2003.)
⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
Theorem	r1funlim 9268	The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 9269 avoids ax-rep 5154.) (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
Theorem	r1fnon 9269	The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ 𝑅1 Fn On
Theorem	r10 9270	Value of the cumulative hierarchy of sets function at ∅. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝑅1‘∅) = ∅
Theorem	r1sucg 9271	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1suc 9272	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ On → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1limg 9273*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1lim 9274*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1fin 9275	The first ω levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.)
⊢ (𝐴 ∈ ω → (𝑅1‘𝐴) ∈ Fin)
Theorem	r1sdom 9276	Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺ (𝑅1‘𝐴))
Theorem	r111 9277	The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ 𝑅1:On–1-1→V
Theorem	r1tr 9278	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ Tr (𝑅1‘𝐴)
Theorem	r1tr2 9279	The union of a cumulative hierarchy of sets at ordinal 𝐴 is a subset of the hierarchy at 𝐴. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011.)
⊢ ∪ (𝑅1‘𝐴) ⊆ (𝑅1‘𝐴)
Theorem	r1ordg 9280	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.)
⊢ (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord3g 9281	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord 9282	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord2 9283	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 22-Sep-2003.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord3 9284	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1sssuc 9285	The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.)
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴))
Theorem	r1pwss 9286	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
Theorem	r1sscl 9287	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵))
Theorem	r1val1 9288*	The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 (𝑅1‘𝑥))
Theorem	tz9.12lem1 9289*	Lemma for tz9.12 9292. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (𝐹 “ 𝐴) ⊆ On
Theorem	tz9.12lem2 9290*	Lemma for tz9.12 9292. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On
Theorem	tz9.12lem3 9291*	Lemma for tz9.12 9292. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝐴 ∈ (𝑅1‘suc suc ∪ (𝐹 “ 𝐴)))
Theorem	tz9.12 9292*	A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 9289 through tz9.12lem3 9291. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦))
Theorem	tz9.13 9293*	Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥)
Theorem	tz9.13g 9294*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9293 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥))
Theorem	rankwflemb 9295*	Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankf 9296	The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ rank:∪ (𝑅1 “ On)⟶On
Theorem	rankon 9297	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ (rank‘𝐴) ∈ On
Theorem	r1elwf 9298	Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	rankvalb 9299*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9318 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankr1ai 9300	One direction of rankr1a 9338. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵)