Home | Metamath
Proof Explorer Theorem List (p. 96 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | inf3lem4 9501* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 29-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β (π΄ β Ο β (πΉβπ΄) β (πΉβsuc π΄))) | ||
Theorem | inf3lem5 9502* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 29-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β ((π΄ β Ο β§ π΅ β π΄) β (πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | inf3lem6 9503* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. (Contributed by NM, 29-Oct-1996.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β πΉ:Οβ1-1βπ« π₯) | ||
Theorem | inf3lem7 9504* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9505 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7880. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.) |
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) & β’ πΉ = (rec(πΊ, β ) βΎ Ο) & β’ π΄ β V & β’ π΅ β V β β’ ((π₯ β β β§ π₯ β βͺ π₯) β Ο β V) | ||
Theorem | inf3 9505 |
Our Axiom of Infinity ax-inf 9508 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 9493, and the conclusion is the version of the Axiom of Infinity
shown as Axiom 7 in [TakeutiZaring] p. 43. (Other standard versions are
proved later as axinf2 9510 and zfinf2 9512.) The main proof is provided by
inf3lema 9494 through inf3lem7 9504, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 9504. This proof is due to
Ian Sutherland, Richard Heck, and Norman Megill and was posted
on Usenet as shown below. Although the result is not new, the authors
were unable to find a published proof.
(As posted to sci.logic on 30-Oct-1996, with annotations added.) Theorem: The statement "There exists a nonempty set that is a subset of its union" implies the Axiom of Infinity. Proof: Let X be a nonempty set which is a subset of its union; the latter property is equivalent to saying that for any y in X, there exists a z in X such that y is in z. Define by finite recursion a function F:omega-->(power X) such that F_0 = 0 (See inf3lemb 9495.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9496.) Note: ^ means intersect, < means \in ("element of"). (Finite recursion as typically done requires the existence of omega; to avoid this we can just use transfinite recursion restricted to omega. F is a class-term that is not necessarily a set at this point.) Lemma 1. F_n subset F_n+1. (See inf3lem1 9498.) Proof: By induction: F_0 subset F_1. If y < F_n+1, then y^X subset F_n, so if F_n subset F_n+1, then y^X subset F_n+1, so y < F_n+2. Lemma 2. F_n =/= X. (See inf3lem2 9499.) Proof: By induction: F_0 =/= X because X is not empty. Assume F_n =/= X. Then there is a y in X that is not in F_n. By definition of X, there is a z in X that contains y. Suppose F_n+1 = X. Then z is in F_n+1, and z^X contains y, so z^X is not a subset of F_n, contrary to the definition of F_n+1. Lemma 3. F_n =/= F_n+1. (See inf3lem3 9500.) Proof: Using the identity y^X subset F_n <-> y^(X-F_n) = 0, we have F_n+1 = {y<X | y^(X-F_n) = 0}. Let q = {y<X-F_n | y^(X-F_n) = 0}. Then q subset F_n+1. Since X-F_n is not empty by Lemma 2 and q is the set of \in-minimal elements of X-F_n, by Foundation q is not empty, so q and therefore F_n+1 have an element not in F_n. Lemma 4. F_n proper_subset F_n+1. (See inf3lem4 9501.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9502.) Proof: Fix m and use induction on n > m. Basis: F_m proper_subset F_m+1 by Lemma 4. Induction: Assume F_m proper_subset F_n. Then since F_n proper_subset F_n+1, F_m proper_subset F_n+1 by transitivity of proper subset. By Lemma 5, F_m =/= F_n for m =/= n, so F is 1-1. (See inf3lem6 9503.) Thus, the inverse of F is a function with range omega and domain a subset of power X, so omega exists by Replacement. (See inf3lem7 9504.) Q.E.D.(Contributed by NM, 29-Oct-1996.) |
β’ βπ₯(π₯ β β β§ π₯ β βͺ π₯) β β’ Ο β V | ||
Theorem | infeq5i 9506 | Half of infeq5 9507. (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ (Ο β V β βπ₯ π₯ β βͺ π₯) | ||
Theorem | infeq5 9507 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex 9513.) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (βπ₯ π₯ β βͺ π₯ β Ο β V) | ||
Axiom | ax-inf 9508* |
Axiom of Infinity. An axiom of Zermelo-Fraenkel set theory. This axiom
is the gateway to "Cantor's paradise" (an expression coined by
Hilbert).
It asserts that given a starting set π₯, an infinite set π¦ built
from it exists. Although our version is apparently not given in the
literature, it is similar to, but slightly shorter than, the Axiom of
Infinity in [FreydScedrov] p. 283
(see inf1 9492 and inf2 9493). More
standard versions, which essentially state that there exists a set
containing all the natural numbers, are shown as zfinf2 9512 and omex 9513 and
are based on the (nontrivial) proof of inf3 9505.
This version has the
advantage that when expanded to primitives, it has fewer symbols than
the standard version ax-inf2 9511. Theorem inf0 9491
shows the reverse
derivation of our axiom from a standard one. Theorem inf5 9515
shows a
very short way to state this axiom.
The standard version of Infinity ax-inf2 9511 requires this axiom along with Regularity ax-reg 9462 for its derivation (as Theorem axinf2 9510 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9511 instead of this one. The derivation of this axiom from ax-inf2 9511 is shown by Theorem axinf 9514. Proofs should normally use the standard version ax-inf2 9511 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.) |
β’ βπ¦(π₯ β π¦ β§ βπ§(π§ β π¦ β βπ€(π§ β π€ β§ π€ β π¦))) | ||
Theorem | zfinf 9509* | Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.) |
β’ βπ₯(π¦ β π₯ β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯))) | ||
Theorem | axinf2 9510* |
A standard version of Axiom of Infinity, expanded to primitives, derived
from our version of Infinity ax-inf 9508 and Regularity ax-reg 9462.
This theorem should not be referenced in any proof. Instead, use ax-inf2 9511 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996.) |
β’ βπ₯(βπ¦(π¦ β π₯ β§ βπ§ Β¬ π§ β π¦) β§ βπ¦(π¦ β π₯ β βπ§(π§ β π₯ β§ βπ€(π€ β π§ β (π€ β π¦ β¨ π€ = π¦))))) | ||
Axiom | ax-inf2 9511* | A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 9512 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9510 above, using our version of Infinity ax-inf 9508 and the Axiom of Regularity ax-reg 9462. We will reference ax-inf2 9511 instead of axinf2 9510 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9508 from ax-inf2 9511 is shown by Theorem axinf 9514. (Contributed by NM, 3-Nov-1996.) |
β’ βπ₯(βπ¦(π¦ β π₯ β§ βπ§ Β¬ π§ β π¦) β§ βπ¦(π¦ β π₯ β βπ§(π§ β π₯ β§ βπ€(π€ β π§ β (π€ β π¦ β¨ π€ = π¦))))) | ||
Theorem | zfinf2 9512* | A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9511 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.) |
β’ βπ₯(β β π₯ β§ βπ¦ β π₯ suc π¦ β π₯) | ||
Theorem | omex 9513 |
The existence of omega (the class of natural numbers). Axiom 7 of
[TakeutiZaring] p. 43. This
theorem is proved assuming the Axiom of
Infinity and in fact is equivalent to it, as shown by the reverse
derivation inf0 9491.
A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial Β¬ Ο β V; this would lead to Ο = On by omon 7805 and Fin = V (the universe of all sets) by fineqv 9141. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 7816 through peano5 7821 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
β’ Ο β V | ||
Theorem | axinf 9514* | The first version of the Axiom of Infinity ax-inf 9508 proved from the second version ax-inf2 9511. Note that we didn't use ax-reg 9462, unlike the other direction axinf2 9510. (Contributed by NM, 24-Apr-2009.) |
β’ βπ¦(π₯ β π¦ β§ βπ§(π§ β π¦ β βπ€(π§ β π€ β§ π€ β π¦))) | ||
Theorem | inf5 9515 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 9507). This provides us with a very compact way to express the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005.) |
β’ βπ₯ π₯ β βͺ π₯ | ||
Theorem | omelon 9516 | Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.) |
β’ Ο β On | ||
Theorem | dfom3 9517* | The class of natural numbers Ο can be defined as the intersection of all inductive sets (which is the smallest inductive set, since inductive sets are closed under intersection), which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82. (Contributed by NM, 6-Aug-1994.) |
β’ Ο = β© {π₯ β£ (β β π₯ β§ βπ¦ β π₯ suc π¦ β π₯)} | ||
Theorem | elom3 9518* | A simplification of elom 7796 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
β’ (π΄ β Ο β βπ₯(Lim π₯ β π΄ β π₯)) | ||
Theorem | dfom4 9519* | A simplification of df-om 7794 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
β’ Ο = {π₯ β£ βπ¦(Lim π¦ β π₯ β π¦)} | ||
Theorem | dfom5 9520 | Ο 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 9521 | 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 9522 | 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 9523 | A finite set is countable (weaker version of isfinite 9522). (Contributed by Thierry Arnoux, 27-Mar-2018.) |
β’ (π΄ β Fin β π΄ βΌ Ο) | ||
Theorem | nnsdom 9524 | 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 9525 | 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 9526 | The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
β’ Ο β suc Ο | ||
Theorem | infdifsn 9527 | 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 9528 | 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 9529* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 9177 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.) |
β’ ((π΄ β Ο β§ βπ₯ β Ο βπ¦ β π΄ π₯ β π¦) β π΄ β Ο) | ||
Theorem | noinfep 9530* | Using the Axiom of Regularity in the form zfregfr 9475, 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 9531 | Extend class notation with the Cantor normal form function. |
class CNF | ||
Definition | df-cnf 9532* | 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 9565 of this function in terms of df-oi 9380. (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 9533* | 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 9534* | 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 9535* | Lemma for cantnf 9563. The function appearing in cantnfval 9538 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.) |
β’ πΉ = seqΟ((π β π΄, π§ β π΅ β¦ (πΆ +o π·)), β ) β β’ πΉ:ΟβΆOn | ||
Theorem | cantnfs 9536 | 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 9537 | 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 9538* | 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 9539* | 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 9540* | 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 9541* | 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 9542* | 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 9543 | 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 9544 | 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 9545 | The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ (π β β β π΄) β β’ (π β ((π΄ CNF π΅)β(π΅ Γ {β })) = β ) | ||
Theorem | cantnfrescl 9546* | 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 9547* | 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 9548* | Lemma for cantnfp1 9551. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ (π β πΊ β π) & β’ (π β π β π΅) & β’ (π β π β π΄) & β’ (π β (πΊ supp β ) β π) & β’ πΉ = (π‘ β π΅ β¦ if(π‘ = π, π, (πΊβπ‘))) β β’ (π β πΉ β π) | ||
Theorem | cantnfp1lem2 9549* | Lemma for cantnfp1 9551. (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 9550* | Lemma for cantnfp1 9551. (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 9551* | 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 9552* | The relation π is a strict order on π (a corollary of wemapso2 9423). (Contributed by Mario Carneiro, 28-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} β β’ (π β π Or π) | ||
Theorem | oemapval 9553* | Value of the relation π. (Contributed by Mario Carneiro, 28-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β πΉ β π) & β’ (π β πΊ β π) β β’ (π β (πΉππΊ β βπ§ β π΅ ((πΉβπ§) β (πΊβπ§) β§ βπ€ β π΅ (π§ β π€ β (πΉβπ€) = (πΊβπ€))))) | ||
Theorem | oemapvali 9554* | 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 9555* | Lemma for cantnf 9563. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β πΉππΊ) & β’ π = βͺ {π β π΅ β£ (πΉβπ) β (πΊβπ)} β β’ (π β π β (πΊ supp β )) | ||
Theorem | cantnflem1b 9556* | Lemma for cantnf 9563. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β πΉππΊ) & β’ π = βͺ {π β π΅ β£ (πΉβπ) β (πΊβπ)} & β’ π = OrdIso( E , (πΊ supp β )) β β’ ((π β§ (suc π’ β dom π β§ (β‘πβπ) β π’)) β π β (πβπ’)) | ||
Theorem | cantnflem1c 9557* | Lemma for cantnf 9563. (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 9558* | Lemma for cantnf 9563. (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 9559* | Lemma for cantnf 9563. 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 9560* | Lemma for cantnf 9563. (Contributed by Mario Carneiro, 28-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} & β’ (π β πΆ β (π΄ βo π΅)) & β’ (π β πΆ β ran (π΄ CNF π΅)) & β’ (π β β β πΆ) β β’ (π β (π΄ β (On β 2o) β§ πΆ β (On β 1o))) | ||
Theorem | cantnflem3 9561* | Lemma for cantnf 9563. 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 8518 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 9551 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 9562* | Lemma for cantnf 9563. Complete the induction step of cantnflem3 9561. (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 9563* | 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 9547, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} β β’ (π β (π΄ CNF π΅) Isom π, E (π, (π΄ βo π΅))) | ||
Theorem | oemapwe 9564* | 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 9565* | An alternate definition of df-cnf 9532 which relies on cantnf 9563. (Note that although the use of π seems self-referential, one can use cantnfdm 9534 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} β β’ (π β (π΄ CNF π΅) = β‘OrdIso(π, π)) | ||
Theorem | cantnff1o 9566 | Simplify the isomorphism of cantnf 9563 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.) |
β’ π = dom (π΄ CNF π΅) & β’ (π β π΄ β On) & β’ (π β π΅ β On) β β’ (π β (π΄ CNF π΅):πβ1-1-ontoβ(π΄ βo π΅)) | ||
Theorem | wemapwe 9567* | 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 9568* | A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (πΉββ ) = β can be discharged using fveqf1o 7244.) (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 9569* | Lemma for cnfcom 9570. (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 9570* | 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 9571* | Lemma for cnfcom2 9572. (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 9572* | 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 9573* | Lemma for cnfcom3 9574. (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 9574* | 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 9576.) (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 9575* | Lemma for cnfcom3c 9576. (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 9576* | Wrap the construction of cnfcom3 9574 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 9577 | Declare the syntax for the transitive closure of a class. |
class t++π | ||
Definition | df-ttrcl 9578* | Define the transitive closure of a class. This is the smallest relationship containing π (or more precisely, the relation (π βΎ V) induced by π ) and having the transitive property. Definition from [Levy] p. 59, who denotes it as π β and calls it the "ancestral" of π . (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ t++π = {β¨π₯, π¦β© β£ βπ β (Ο β 1o)βπ(π Fn suc π β§ ((πββ ) = π₯ β§ (πβπ) = π¦) β§ βπ β π (πβπ)π (πβsuc π))} | ||
Theorem | ttrcleq 9579 | Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (π = π β t++π = t++π) | ||
Theorem | nfttrcld 9580 | Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.) |
β’ (π β β²π₯π ) β β’ (π β β²π₯t++π ) | ||
Theorem | nfttrcl 9581 | Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ β²π₯π β β’ β²π₯t++π | ||
Theorem | relttrcl 9582 | The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ Rel t++π | ||
Theorem | brttrcl 9583* | Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.) |
β’ (π΄t++π π΅ β βπ β (Ο β 1o)βπ(π Fn suc π β§ ((πββ ) = π΄ β§ (πβπ) = π΅) β§ βπ β π (πβπ)π (πβsuc π))) | ||
Theorem | brttrcl2 9584* | 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 9585 | If π is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (Rel π β π β t++π ) | ||
Theorem | ttrcltr 9586 | The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (t++π β t++π ) β t++π | ||
Theorem | ttrclresv 9587 | 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 9588 | Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.) |
β’ (t++π β π ) β t++π | ||
Theorem | cottrcl 9589 | Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.) |
β’ (π β t++π ) β t++π | ||
Theorem | ttrclss 9590 | 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 9591 | 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 9592 | 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 9593 | If π is a set, then so is t++π . (Contributed by Scott Fenton, 26-Oct-2024.) |
β’ (π β π β t++π β V) | ||
Theorem | dfttrcl2 9594* | When π is a set and a relationship, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024.) |
β’ ((π β π β§ Rel π ) β t++π = β© {π§ β£ (π β π§ β§ (π§ β π§) β π§)}) | ||
Theorem | ttrclselem1 9595* | Lemma for ttrclse 9597. Show that all finite ordinal function values of πΉ are subsets of π΄. (Contributed by Scott Fenton, 31-Oct-2024.) |
β’ πΉ = rec((π β V β¦ βͺ π€ β π Pred(π , π΄, π€)), Pred(π , π΄, π)) β β’ (π β Ο β (πΉβπ) β π΄) | ||
Theorem | ttrclselem2 9596* | Lemma for ttrclse 9597. 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 9597 |
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 9598* | 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 9599 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 9599* |
Every set has a transitive closure (the smallest transitive extension).
Theorem 9.1 of [TakeutiZaring] p.
73. See trcl 9598 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 9600* | Alternate expression for the existence of transitive closures tz9.1 9599: the intersection of all transitive sets containing π΄ is a set. (Contributed by Mario Carneiro, 22-Mar-2013.) |
β’ π΄ β V β β’ β© {π₯ β£ (π΄ β π₯ β§ Tr π₯)} β V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |