Home | Metamath
Proof Explorer Theorem List (p. 92 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfom4 9101* | A simplification of df-om 7569 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom5 9102 | ω 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 9103 | 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 9104 | 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 9105 | A finite set is countable (weaker version of isfinite 9104). (Contributed by Thierry Arnoux, 27-Mar-2018.) |
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω) | ||
Theorem | nnsdom 9106 | 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 9107 | 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 9108 | The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ω ≈ suc ω | ||
Theorem | infdifsn 9109 | 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 9110 | 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 9111* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 8763 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.) |
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | noinfep 9112* | Using the Axiom of Regularity in the form zfregfr 9057, 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 𝑥) ∉ (𝐹‘𝑥) | ||
Syntax | ccnf 9113 | Extend class notation with the Cantor normal form function. |
class CNF | ||
Definition | df-cnf 9114* | 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 9147 of this function in terms of df-oi 8963. (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 9115* | 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 9116* | 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 9117* | Lemma for cantnf 9145. The function appearing in cantnfval 9120 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ 𝐹 = seqω((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +o 𝐷)), ∅) ⇒ ⊢ 𝐹:ω⟶On | ||
Theorem | cantnfs 9118 | 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 9119 | 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 9120* | 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 9121* | 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 9122* | 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 9123* | 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 9124* | 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 9125 | 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 9126 | 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 9127 | The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → ∅ ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅) | ||
Theorem | cantnfrescl 9128* | 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 9129* | 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 9130* | Lemma for cantnfp1 9133. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑆) | ||
Theorem | cantnfp1lem2 9131* | Lemma for cantnfp1 9133. (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 9132* | Lemma for cantnfp1 9133. (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 9133* | 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 9134* | The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 9006). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → 𝑇 Or 𝑆) | ||
Theorem | oemapval 9135* | Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) | ||
Theorem | oemapvali 9136* | 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 9137* | Lemma for cantnf 9145. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | cantnflem1b 9138* | Lemma for cantnf 9145. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) ⇒ ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢)) | ||
Theorem | cantnflem1c 9139* | Lemma for cantnf 9145. (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 9140* | Lemma for cantnf 9145. (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 9141* | Lemma for cantnf 9145. 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 9142* | Lemma for cantnf 9145. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o))) | ||
Theorem | cantnflem3 9143* | Lemma for cantnf 9145. 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 8219 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 9133 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 9144* | Lemma for cantnf 9145. Complete the induction step of cantnflem3 9143. (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 9145* | 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 9129, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑o 𝐵))) | ||
Theorem | oemapwe 9146* | 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 9147* | An alternate definition of df-cnf 9114 which relies on cantnf 9145. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 9116 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆)) | ||
Theorem | cantnff1o 9148 | Simplify the isomorphism of cantnf 9145 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑o 𝐵)) | ||
Theorem | wemapwe 9149* | 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 9150* | A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 7049.) (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 9151* | Lemma for cnfcom 9152. (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 9152* | 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 9153* | Lemma for cnfcom2 9154. (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 9154* | 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 9155* | Lemma for cnfcom3 9156. (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 9156* | 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 9158.) (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 9157* | Lemma for cnfcom3c 9158. (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 9158* | Wrap the construction of cnfcom3 9156 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 𝑤))) | ||
Theorem | trcl 9159* | 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 9160 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 9160* |
Every set has a transitive closure (the smallest transitive extension).
Theorem 9.1 of [TakeutiZaring] p.
73. See trcl 9159 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 9161* | Alternate expression for the existence of transitive closures tz9.1 9160: the intersection of all transitive sets containing 𝐴 is a set. (Contributed by Mario Carneiro, 22-Mar-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V | ||
Theorem | epfrs 9162* | The strong form of the Axiom of Regularity (no sethood requirement on 𝐴), with the axiom itself present as an antecedent. See also zfregs 9163. (Contributed by Mario Carneiro, 22-Mar-2013.) |
⊢ (( E Fr 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | zfregs 9163* | 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 9162. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | zfregs2 9164* | 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 9165* | Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.) |
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V) | ||
Theorem | setind2 9166 | 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 9167 | Extend class notation to include the transitive closure function. |
class TC | ||
Definition | df-tc 9168* | The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)}) | ||
Theorem | tcvalg 9169* | Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 9090; see tz9.1 9160.) (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (𝐴 ∈ 𝑉 → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) | ||
Theorem | tcid 9170 | Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (TC‘𝐴)) | ||
Theorem | tctr 9171 | Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ Tr (TC‘𝐴) | ||
Theorem | tcmin 9172 | 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 9173* | 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 9174 | The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (TC‘{𝐴}) = ((TC‘𝐴) ∪ {𝐴}) | ||
Theorem | tcss 9175 | The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ⊆ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcel 9176 | The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴)) | ||
Theorem | tcidm 9177 | The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ (TC‘(TC‘𝐴)) = (TC‘𝐴) | ||
Theorem | tc0 9178 | The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (TC‘∅) = ∅ | ||
Theorem | tc00 9179 | The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Syntax | cr1 9180 | Extend class definition to include the cumulative hierarchy of sets function. |
class 𝑅1 | ||
Syntax | crnk 9181 | Extend class definition to include rank function. |
class rank | ||
Definition | df-r1 9182 | 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 9209). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 9186, r1suc 9188, and r1lim 9190. Theorem r1val1 9204 shows a recursive definition that works for all values, and theorems r1val2 9255 and r1val3 9256 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 9183* | Define the rank function. See rankval 9234, rankval2 9236, rankval3 9258, or rankval4 9285 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 9251 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9254. (Contributed by NM, 11-Oct-2003.) |
⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)}) | ||
Theorem | r1funlim 9184 | The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 9185 avoids ax-rep 5182.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1) | ||
Theorem | r1fnon 9185 | 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 9186 | 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 9187 | 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 9188 | 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 9189* | 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 9190* | 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 9191 | The first ω levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.) |
⊢ (𝐴 ∈ ω → (𝑅1‘𝐴) ∈ Fin) | ||
Theorem | r1sdom 9192 | Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺ (𝑅1‘𝐴)) | ||
Theorem | r111 9193 | The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.) |
⊢ 𝑅1:On–1-1→V | ||
Theorem | r1tr 9194 | 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 9195 | 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 9196 | 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 9197 | 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 9198 | 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 9199 | 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 9200 | 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‘𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |