![]() |
Metamath
Proof Explorer Theorem List (p. 98 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnfcom3 9701* | 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 9703.) (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 9702* | Lemma for cnfcom3c 9703. (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 9703* | Wrap the construction of cnfcom3 9701 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 9704 | Declare the syntax for the transitive closure of a class. |
class t++π | ||
Definition | df-ttrcl 9705* | 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 9706 | Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (π = π β t++π = t++π) | ||
Theorem | nfttrcld 9707 | Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.) |
β’ (π β β²π₯π ) β β’ (π β β²π₯t++π ) | ||
Theorem | nfttrcl 9708 | Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ β²π₯π β β’ β²π₯t++π | ||
Theorem | relttrcl 9709 | The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ Rel t++π | ||
Theorem | brttrcl 9710* | Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.) |
β’ (π΄t++π π΅ β βπ β (Ο β 1o)βπ(π Fn suc π β§ ((πββ ) = π΄ β§ (πβπ) = π΅) β§ βπ β π (πβπ)π (πβsuc π))) | ||
Theorem | brttrcl2 9711* | 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 9712 | If π is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (Rel π β π β t++π ) | ||
Theorem | ttrcltr 9713 | The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.) |
β’ (t++π β t++π ) β t++π | ||
Theorem | ttrclresv 9714 | 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 9715 | Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.) |
β’ (t++π β π ) β t++π | ||
Theorem | cottrcl 9716 | Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.) |
β’ (π β t++π ) β t++π | ||
Theorem | ttrclss 9717 | 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 9718 | 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 9719 | 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 9720 | If π is a set, then so is t++π . (Contributed by Scott Fenton, 26-Oct-2024.) |
β’ (π β π β t++π β V) | ||
Theorem | dfttrcl2 9721* | 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 9722* | Lemma for ttrclse 9724. Show that all finite ordinal function values of πΉ are subsets of π΄. (Contributed by Scott Fenton, 31-Oct-2024.) |
β’ πΉ = rec((π β V β¦ βͺ π€ β π Pred(π , π΄, π€)), Pred(π , π΄, π)) β β’ (π β Ο β (πΉβπ) β π΄) | ||
Theorem | ttrclselem2 9723* | Lemma for ttrclse 9724. 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 9724 |
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 9725* | 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 9726 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 9726* |
Every set has a transitive closure (the smallest transitive extension).
Theorem 9.1 of [TakeutiZaring] p.
73. See trcl 9725 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 9727* | Alternate expression for the existence of transitive closures tz9.1 9726: the intersection of all transitive sets containing π΄ is a set. (Contributed by Mario Carneiro, 22-Mar-2013.) |
β’ π΄ β V β β’ β© {π₯ β£ (π΄ β π₯ β§ Tr π₯)} β V | ||
Theorem | epfrs 9728* | The strong form of the Axiom of Regularity (no sethood requirement on π΄), with the axiom itself present as an antecedent. See also zfregs 9729. (Contributed by Mario Carneiro, 22-Mar-2013.) |
β’ (( E Fr π΄ β§ π΄ β β ) β βπ₯ β π΄ (π₯ β© π΄) = β ) | ||
Theorem | zfregs 9729* | 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 9728. (Contributed by NM, 17-Sep-2003.) |
β’ (π΄ β β β βπ₯ β π΄ (π₯ β© π΄) = β ) | ||
Theorem | zfregs2 9730* | 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 9731* | Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.) |
β’ (βπ₯(π₯ β π΄ β π₯ β π΄) β π΄ = V) | ||
Theorem | setind2 9732 | 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 9733 | Extend class notation to include the transitive closure function. |
class TC | ||
Definition | df-tc 9734* | The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ TC = (π₯ β V β¦ β© {π¦ β£ (π₯ β π¦ β§ Tr π¦)}) | ||
Theorem | tcvalg 9735* | Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 9635; see tz9.1 9726.) (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ (π΄ β π β (TCβπ΄) = β© {π₯ β£ (π΄ β π₯ β§ Tr π₯)}) | ||
Theorem | tcid 9736 | Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ (π΄ β π β π΄ β (TCβπ΄)) | ||
Theorem | tctr 9737 | Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ Tr (TCβπ΄) | ||
Theorem | tcmin 9738 | 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 9739* | 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 9740 | The transitive closure of a singleton. Proof suggested by GΓ©rard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.) |
β’ π΄ β V β β’ (TCβ{π΄}) = ((TCβπ΄) βͺ {π΄}) | ||
Theorem | tcss 9741 | The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ π΄ β V β β’ (π΅ β π΄ β (TCβπ΅) β (TCβπ΄)) | ||
Theorem | tcel 9742 | The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ π΄ β V β β’ (π΅ β π΄ β (TCβπ΅) β (TCβπ΄)) | ||
Theorem | tcidm 9743 | The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.) |
β’ (TCβ(TCβπ΄)) = (TCβπ΄) | ||
Theorem | tc0 9744 | The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.) |
β’ (TCββ ) = β | ||
Theorem | tc00 9745 | 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 9746* | 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 6348 and tz7.5 6385. (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 9747* | 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 6351 and tfi 7844, 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 9748* | 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 9749* | 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 9750* | 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 9751* | 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 9752* | 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 9753* | Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 9758. (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ (((π Fr π΄ β§ π Se π΄) β§ (πΉ Fn π΄ β§ βπ¦ β π΄ (πΉβπ¦) = (π¦π»(πΉ βΎ Pred(π , π΄, π¦)))) β§ (πΊ Fn π΄ β§ βπ¦ β π΄ (πΊβπ¦) = (π¦π»(πΊ βΎ Pred(π , π΄, π¦))))) β πΉ = πΊ) | ||
Theorem | frrlem15 9754* | 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 9755* | 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 9756 | Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 8290, fpr2 8291, and fpr3 8292, which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023.) |
β’ πΉ = frecs(π , π΄, πΊ) β β’ ((π Fr π΄ β§ π Se π΄) β πΉ Fn π΄) | ||
Theorem | frr2 9757 | 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 9758* | 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 9756 and frr2 9757 is identical to πΉ. (Contributed by Scott Fenton, 11-Sep-2023.) |
β’ πΉ = frecs(π , π΄, πΊ) β β’ (((π Fr π΄ β§ π Se π΄) β§ (π» Fn π΄ β§ βπ§ β π΄ (π»βπ§) = (π§πΊ(π» βΎ Pred(π , π΄, π§))))) β πΉ = π») | ||
Syntax | cr1 9759 | Extend class definition to include the cumulative hierarchy of sets function. |
class π 1 | ||
Syntax | crnk 9760 | Extend class definition to include rank function. |
class rank | ||
Definition | df-r1 9761 | 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 9788). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as Theorems r10 9765, r1suc 9767, and r1lim 9769. Theorem r1val1 9783 shows a recursive definition that works for all values, and Theorems r1val2 9834 and r1val3 9835 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 9762* | Define the rank function. See rankval 9813, rankval2 9815, rankval3 9837, or rankval4 9864 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 9830 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9833. (Contributed by NM, 11-Oct-2003.) |
β’ rank = (π₯ β V β¦ β© {π¦ β On β£ π₯ β (π 1βsuc π¦)}) | ||
Theorem | r1funlim 9763 | The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 9764 avoids ax-rep 5285.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ (Fun π 1 β§ Lim dom π 1) | ||
Theorem | r1fnon 9764 | 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 9765 | 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 9766 | 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 9767 | 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 9768* | 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 9769* | 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 9770 | The first Ο levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.) |
β’ (π΄ β Ο β (π 1βπ΄) β Fin) | ||
Theorem | r1sdom 9771 | Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.) |
β’ ((π΄ β On β§ π΅ β π΄) β (π 1βπ΅) βΊ (π 1βπ΄)) | ||
Theorem | r111 9772 | The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.) |
β’ π 1:Onβ1-1βV | ||
Theorem | r1tr 9773 | 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 9774 | 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 9775 | 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 9776 | 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 9777 | 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 9778 | 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 9779 | Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ β π΅ β (π 1βπ΄) β (π 1βπ΅))) | ||
Theorem | r1sssuc 9780 | The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.) |
β’ (π΄ β On β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | r1pwss 9781 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β (π 1βπ΅) β π« π΄ β (π 1βπ΅)) | ||
Theorem | r1sscl 9782 | Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ ((π΄ β (π 1βπ΅) β§ πΆ β π΄) β πΆ β (π 1βπ΅)) | ||
Theorem | r1val1 9783* | The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ (π΄ β dom π 1 β (π 1βπ΄) = βͺ π₯ β π΄ π« (π 1βπ₯)) | ||
Theorem | tz9.12lem1 9784* | Lemma for tz9.12 9787. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ π΄ β V & β’ πΉ = (π§ β V β¦ β© {π£ β On β£ π§ β (π 1βπ£)}) β β’ (πΉ β π΄) β On | ||
Theorem | tz9.12lem2 9785* | Lemma for tz9.12 9787. (Contributed by NM, 22-Sep-2003.) |
β’ π΄ β V & β’ πΉ = (π§ β V β¦ β© {π£ β On β£ π§ β (π 1βπ£)}) β β’ suc βͺ (πΉ β π΄) β On | ||
Theorem | tz9.12lem3 9786* | Lemma for tz9.12 9787. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ π΄ β V & β’ πΉ = (π§ β V β¦ β© {π£ β On β£ π§ β (π 1βπ£)}) β β’ (βπ₯ β π΄ βπ¦ β On π₯ β (π 1βπ¦) β π΄ β (π 1βsuc suc βͺ (πΉ β π΄))) | ||
Theorem | tz9.12 9787* | A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 9784 through tz9.12lem3 9786. (Contributed by NM, 22-Sep-2003.) |
β’ π΄ β V β β’ (βπ₯ β π΄ βπ¦ β On π₯ β (π 1βπ¦) β βπ¦ β On π΄ β (π 1βπ¦)) | ||
Theorem | tz9.13 9788* | Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.) |
β’ π΄ β V β β’ βπ₯ β On π΄ β (π 1βπ₯) | ||
Theorem | tz9.13g 9789* | Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9788 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.) |
β’ (π΄ β π β βπ₯ β On π΄ β (π 1βπ₯)) | ||
Theorem | rankwflemb 9790* | Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β βͺ (π 1 β On) β βπ₯ β On π΄ β (π 1βsuc π₯)) | ||
Theorem | rankf 9791 | The domain and codomain of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.) |
β’ rank:βͺ (π 1 β On)βΆOn | ||
Theorem | rankon 9792 | The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.) |
β’ (rankβπ΄) β On | ||
Theorem | r1elwf 9793 | Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
β’ (π΄ β (π 1βπ΅) β π΄ β βͺ (π 1 β On)) | ||
Theorem | rankvalb 9794* | Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9813 does not use Regularity, and so requires the assumption that π΄ is in the range of π 1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
β’ (π΄ β βͺ (π 1 β On) β (rankβπ΄) = β© {π₯ β On β£ π΄ β (π 1βsuc π₯)}) | ||
Theorem | rankr1ai 9795 | One direction of rankr1a 9833. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ (π΄ β (π 1βπ΅) β (rankβπ΄) β π΅) | ||
Theorem | rankvaln 9796 | Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 9810, unless π΄ is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.) |
β’ (Β¬ π΄ β βͺ (π 1 β On) β (rankβπ΄) = β ) | ||
Theorem | rankidb 9797 | Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.) |
β’ (π΄ β βͺ (π 1 β On) β π΄ β (π 1βsuc (rankβπ΄))) | ||
Theorem | rankdmr1 9798 | A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.) |
β’ (rankβπ΄) β dom π 1 | ||
Theorem | rankr1ag 9799 | A version of rankr1a 9833 that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ ((π΄ β βͺ (π 1 β On) β§ π΅ β dom π 1) β (π΄ β (π 1βπ΅) β (rankβπ΄) β π΅)) | ||
Theorem | rankr1bg 9800 | A relationship between rank and π 1. See rankr1ag 9799 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.) |
β’ ((π΄ β βͺ (π 1 β On) β§ π΅ β dom π 1) β (π΄ β (π 1βπ΅) β (rankβπ΄) β π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |