![]() |
Metamath
Proof Explorer Theorem List (p. 98 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cantnfdm 9701* | 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 9702* | Lemma for cantnf 9730. The function appearing in cantnfval 9705 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅) ⇒ ⊢ 𝐹:ω⟶On | ||
Theorem | cantnfs 9703 | 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 9704 | 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 9705* | 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 9706* | 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 9707* | 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 9708* | 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 9709* | 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 9710 | 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 9711 | 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 9712 | The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → ∅ ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅) | ||
Theorem | cantnfrescl 9713* | 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 9714* | 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 9715* | Lemma for cantnfp1 9718. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑆) | ||
Theorem | cantnfp1lem2 9716* | Lemma for cantnfp1 9718. (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 9717* | Lemma for cantnfp1 9718. (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 9718* | 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 9719* | The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9590). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → 𝑇 Or 𝑆) | ||
Theorem | oemapval 9720* | Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) | ||
Theorem | oemapvali 9721* | 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 9722* | Lemma for cantnf 9730. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | cantnflem1b 9723* | Lemma for cantnf 9730. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) ⇒ ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢)) | ||
Theorem | cantnflem1c 9724* | Lemma for cantnf 9730. (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 9725* | Lemma for cantnf 9730. (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 9726* | Lemma for cantnf 9730. 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 9727* | Lemma for cantnf 9730. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o))) | ||
Theorem | cantnflem3 9728* | Lemma for cantnf 9730. 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 8639 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 9718 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 9729* | Lemma for cantnf 9730. Complete the induction step of cantnflem3 9728. (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 9730* | 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 9714, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵))) | ||
Theorem | oemapwe 9731* | 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 9732* | An alternate definition of df-cnf 9699 which relies on cantnf 9730. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9701 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆)) | ||
Theorem | cantnff1o 9733 | Simplify the isomorphism of cantnf 9730 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵)) | ||
Theorem | wemapwe 9734* | 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 9735* | A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7321.) (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 9736* | Lemma for cnfcom 9737. (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 9737* | 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 9738* | Lemma for cnfcom2 9739. (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 9739* | 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 9740* | Lemma for cnfcom3 9741. (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 9741* | 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 9743.) (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 9742* | Lemma for cnfcom3c 9743. (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 9743* | Wrap the construction of cnfcom3 9741 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 𝑤))) | ||
Syntax | cttrcl 9744 | Declare the syntax for the transitive closure of a class. |
class t++𝑅 | ||
Definition | df-ttrcl 9745* | Define the transitive closure of a class. This is the smallest relation 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 9746 | Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
⊢ (𝑅 = 𝑆 → t++𝑅 = t++𝑆) | ||
Theorem | nfttrcld 9747 | Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.) |
⊢ (𝜑 → Ⅎ𝑥𝑅) ⇒ ⊢ (𝜑 → Ⅎ𝑥t++𝑅) | ||
Theorem | nfttrcl 9748 | Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥t++𝑅 | ||
Theorem | relttrcl 9749 | The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.) |
⊢ Rel t++𝑅 | ||
Theorem | brttrcl 9750* | Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.) |
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘𝑛) = 𝐵) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))) | ||
Theorem | brttrcl2 9751* | 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 9752 | If 𝑅 is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅) | ||
Theorem | ttrcltr 9753 | The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.) |
⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅 | ||
Theorem | ttrclresv 9754 | 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 9755 | Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.) |
⊢ (t++𝑅 ∘ 𝑅) ⊆ t++𝑅 | ||
Theorem | cottrcl 9756 | Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.) |
⊢ (𝑅 ∘ t++𝑅) ⊆ t++𝑅 | ||
Theorem | ttrclss 9757 | 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 9758 | 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 9759 | 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 9760 | If 𝑅 is a set, then so is t++𝑅. (Contributed by Scott Fenton, 26-Oct-2024.) |
⊢ (𝑅 ∈ 𝑉 → t++𝑅 ∈ V) | ||
Theorem | dfttrcl2 9761* | When 𝑅 is a set and a relation, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → t++𝑅 = ∩ {𝑧 ∣ (𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | ||
Theorem | ttrclselem1 9762* | Lemma for ttrclse 9764. Show that all finite ordinal function values of 𝐹 are subsets of 𝐴. (Contributed by Scott Fenton, 31-Oct-2024.) |
⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋)) ⇒ ⊢ (𝑁 ∈ ω → (𝐹‘𝑁) ⊆ 𝐴) | ||
Theorem | ttrclselem2 9763* | Lemma for ttrclse 9764. 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 9764 |
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 𝐴) | ||
Theorem | trcl 9765* | 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 9766 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 9766* |
Every set has a transitive closure (the smallest transitive extension).
Theorem 9.1 of [TakeutiZaring] p.
73. See trcl 9765 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 9767* | Alternate expression for the existence of transitive closures tz9.1 9766: the intersection of all transitive sets containing 𝐴 is a set. (Contributed by Mario Carneiro, 22-Mar-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V | ||
Theorem | epfrs 9768* | The strong form of the Axiom of Regularity (no sethood requirement on 𝐴), with the axiom itself present as an antecedent. See also zfregs 9769. (Contributed by Mario Carneiro, 22-Mar-2013.) |
⊢ (( E Fr 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | zfregs 9769* | 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 9768. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | zfregs2 9770* | 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 9771* | Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.) |
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V) | ||
Theorem | setind2 9772 | 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 9773 | Extend class notation to include the transitive closure function. |
class TC | ||
Definition | df-tc 9774* | The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}) | ||
Theorem | tcvalg 9775* | Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 9675; see tz9.1 9766.) (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (𝐴 ∈ 𝑉 → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) | ||
Theorem | tcid 9776 | Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (TC‘𝐴)) | ||
Theorem | tctr 9777 | Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ Tr (TC‘𝐴) | ||
Theorem | tcmin 9778 | 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 9779* | 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 9780 | The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (TC‘{𝐴}) = ((TC‘𝐴) ∪ {𝐴}) | ||
Theorem | tcss 9781 | The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ⊆ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcel 9782 | The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcidm 9783 | The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (TC‘(TC‘𝐴)) = (TC‘𝐴) | ||
Theorem | tc0 9784 | The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (TC‘∅) = ∅ | ||
Theorem | tc00 9785 | The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Theorem | frmin 9786* | Every (possibly proper) subclass of a class 𝐴 with a well-founded set-like relation 𝑅 has a minimal element. This is a very strong generalization of tz6.26 6369 and tz7.5 6406. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 27-Nov-2024.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | frind 9787* | A subclass of a well-founded class 𝐴 with the property that whenever it contains all predecessors of an element of 𝐴 it also contains that element, is equal to 𝐴. Compare wfi 6372 and tfi 7873, which are special cases of this theorem that do not require the axiom of infinity. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frinsg 9788* | Well-Founded Induction Schema. If a property passes from all elements less than 𝑦 of a well-founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. Theorem 5.6(ii) of [Levy] p. 64. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins 9789* | Well-Founded Induction Schema. If a property passes from all elements less than 𝑦 of a well-founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | frins2f 9790* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins2 9791* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 8-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins3 9792* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒) | ||
Theorem | frr3g 9793* | Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 9798. (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | frrlem15 9794* | Lemma for general well-founded recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | frrlem16 9795* | Lemma for general well-founded recursion. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023.) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ Pred (t++(𝑅 ↾ 𝐴), 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(t++(𝑅 ↾ 𝐴), 𝐴, 𝑧)) | ||
Theorem | frr1 9796 | Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 8326, fpr2 8327, and fpr3 8328, which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
Theorem | frr2 9797 | Law of general well-founded recursion, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | frr3 9798* | Law of general well-founded recursion, part three. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in frr1 9796 and frr2 9797 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Syntax | cr1 9799 | Extend class definition to include the cumulative hierarchy of sets function. |
class 𝑅1 | ||
Syntax | crnk 9800 | Extend class definition to include rank function. |
class rank |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |