![]() |
Metamath
Proof Explorer Theorem List (p. 108 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cina 10701 | The class of strong inaccessibles. |
class Inacc | ||
Definition | df-wina 10702* | An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows Ο as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ Inaccw = {π₯ β£ (π₯ β β β§ (cfβπ₯) = π₯ β§ βπ¦ β π₯ βπ§ β π₯ π¦ βΊ π§)} | ||
Definition | df-ina 10703* | An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ Inacc = {π₯ β£ (π₯ β β β§ (cfβπ₯) = π₯ β§ βπ¦ β π₯ π« π¦ βΊ π₯)} | ||
Theorem | elwina 10704* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inaccw β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | elina 10705* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inacc β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ π« π₯ βΊ π΄)) | ||
Theorem | winaon 10706 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β π΄ β On) | ||
Theorem | inawinalem 10707* | Lemma for inawina 10708. (Contributed by Mario Carneiro, 8-Jun-2014.) |
β’ (π΄ β On β (βπ₯ β π΄ π« π₯ βΊ π΄ β βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | inawina 10708 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inacc β π΄ β Inaccw) | ||
Theorem | omina 10709 | Ο is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow Ο as an inaccessible cardinal, but this choice allows to reuse our results for inaccessibles for Ο.) (Contributed by Mario Carneiro, 29-May-2014.) |
β’ Ο β Inacc | ||
Theorem | winacard 10710 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β (cardβπ΄) = π΄) | ||
Theorem | winainflem 10711* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β β β§ π΄ β On β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) β Ο β π΄) | ||
Theorem | winainf 10712 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Ο β π΄) | ||
Theorem | winalim 10713 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Lim π΄) | ||
Theorem | winalim2 10714* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯)) | ||
Theorem | winafp 10715 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β (β΅βπ΄) = π΄) | ||
Theorem | winafpi 10716 | This theorem, which states that a nontrivial inaccessible cardinal is its own aleph number, is stated here in inference form, where the assumptions are in the hypotheses rather than an antecedent. Often, we use dedth 4583 to turn this type of statement into the closed form statement winafp 10715, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10715 using this theorem and dedth 4583, in ZFC. (You can prove this if you use ax-groth 10841, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
β’ π΄ β Inaccw & β’ π΄ β Ο β β’ (β΅βπ΄) = π΄ | ||
Theorem | gchina 10717 | Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 5-Jun-2015.) |
β’ (GCH = V β Inaccw = Inacc) | ||
Syntax | cwun 10718 | Extend class definition to include the class of all weak universes. |
class WUni | ||
Syntax | cwunm 10719 | Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset. |
class wUniCl | ||
Definition | df-wun 10720* | The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun 10758) whereas the analogue for Grothendieck universes requires ax-groth 10841 (see grothtsk 10853). (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ WUni = {π’ β£ (Tr π’ β§ π’ β β β§ βπ₯ β π’ (βͺ π₯ β π’ β§ π« π₯ β π’ β§ βπ¦ β π’ {π₯, π¦} β π’))} | ||
Definition | df-wunc 10721* | A function that maps a set π₯ to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ wUniCl = (π₯ β V β¦ β© {π’ β WUni β£ π₯ β π’}) | ||
Theorem | iswun 10722* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β (π β WUni β (Tr π β§ π β β β§ βπ₯ β π (βͺ π₯ β π β§ π« π₯ β π β§ βπ¦ β π {π₯, π¦} β π)))) | ||
Theorem | wuntr 10723 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β WUni β Tr π) | ||
Theorem | wununi 10724 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β βͺ π΄ β π) | ||
Theorem | wunpw 10725 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | wunelss 10726 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π΄ β π) | ||
Theorem | wunpr 10727 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | wunun 10728 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | wuntp 10729 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β {π΄, π΅, πΆ} β π) | ||
Theorem | wunss 10730 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | wunin 10731 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β© π΅) β π) | ||
Theorem | wundif 10732 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wunint 10733 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ ((π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | wunsn 10734 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | wunsuc 10735 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β suc π΄ β π) | ||
Theorem | wun0 10736 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β β β π) | ||
Theorem | wunr1om 10737 | A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β (π 1 β Ο) β π) | ||
Theorem | wunom 10738 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β Ο β π) | ||
Theorem | wunfi 10739 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β π΄ β π) | ||
Theorem | wunop 10740 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β¨π΄, π΅β© β π) | ||
Theorem | wunot 10741 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β β¨π΄, π΅, πΆβ© β π) | ||
Theorem | wunxp 10742 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ Γ π΅) β π) | ||
Theorem | wunpm 10743 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βpm π΅) β π) | ||
Theorem | wunmap 10744 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βm π΅) β π) | ||
Theorem | wunf 10745 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β πΉ β π) | ||
Theorem | wundm 10746 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β dom π΄ β π) | ||
Theorem | wunrn 10747 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β ran π΄ β π) | ||
Theorem | wuncnv 10748 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β β‘π΄ β π) | ||
Theorem | wunres 10749 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ βΎ π΅) β π) | ||
Theorem | wunfv 10750 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄βπ΅) β π) | ||
Theorem | wunco 10751 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wuntpos 10752 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β tpos π΄ β π) | ||
Theorem | intwun 10753 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β WUni β§ π΄ β β ) β β© π΄ β WUni) | ||
Theorem | r1limwun 10754 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β π β§ Lim π΄) β (π 1βπ΄) β WUni) | ||
Theorem | r1wunlim 10755 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β ((π 1βπ΄) β WUni β Lim π΄)) | ||
Theorem | wunex2 10756* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) & β’ π = βͺ ran πΉ β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wunex 10757* | Construct a weak universe from a given set. See also wunex2 10756. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β βπ’ β WUni π΄ β π’) | ||
Theorem | uniwun 10758 | Every set is contained in a weak universe. This is the analogue of grothtsk 10853 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10853. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ βͺ WUni = V | ||
Theorem | wunex3 10759 | Construct a weak universe from a given set. This version of wunex 10757 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π = (π 1β((rankβπ΄) +o Ο)) β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wuncval 10760* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) = β© {π’ β WUni β£ π΄ β π’}) | ||
Theorem | wuncid 10761 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β π΄ β (wUniClβπ΄)) | ||
Theorem | wunccl 10762 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) β WUni) | ||
Theorem | wuncss 10763 | The weak universe closure is a subset of any other weak universe containing the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π β WUni β§ π΄ β π) β (wUniClβπ΄) β π) | ||
Theorem | wuncidm 10764 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβ(wUniClβπ΄)) = (wUniClβπ΄)) | ||
Theorem | wuncval2 10765* | Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) & β’ π = βͺ ran πΉ β β’ (π΄ β π β (wUniClβπ΄) = π) | ||
Syntax | ctsk 10766 | Extend class definition to include the class of all Tarski classes. |
class Tarski | ||
Definition | df-tsk 10767* | The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his article Tarski's Classes and Ranks, Journal of Formalized Mathematics, Vol 1, No 3, May-August 1990. A Tarski class is a set whose existence is ensured by Tarski's Axiom A (see ax-groth 10841 and the equivalent axioms). Axiom A was first presented in Tarski's article Ueber unerreichbare Kardinalzahlen. Tarski introduced Axiom A to allow reasoning with inaccessible cardinals in ZFC. Later, Grothendieck introduced the concept of (Grothendieck) universes and showed they were exactly transitive Tarski classes. (Contributed by FL, 30-Dec-2010.) |
β’ Tarski = {π¦ β£ (βπ§ β π¦ (π« π§ β π¦ β§ βπ€ β π¦ π« π§ β π€) β§ βπ§ β π« π¦(π§ β π¦ β¨ π§ β π¦))} | ||
Theorem | eltskg 10768* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ βπ€ β π π« π§ β π€) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | eltsk2g 10769* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ π« π§ β π) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | tskpwss 10770 | First axiom of a Tarski class. The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β π) β π« π΄ β π) | ||
Theorem | tskpw 10771 | Second axiom of a Tarski class. The powerset of an element of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β π) β π« π΄ β π) | ||
Theorem | tsken 10772 | Third axiom of a Tarski class. A subset of a Tarski class is either equipotent to the class or an element of the class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β π) β (π΄ β π β¨ π΄ β π)) | ||
Theorem | 0tsk 10773 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ β β Tarski | ||
Theorem | tsksdom 10774 | An element of a Tarski class is strictly dominated by the class. JFM CLASSES2 th. 1. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β π) β π΄ βΊ π) | ||
Theorem | tskssel 10775 | A part of a Tarski class strictly dominated by the class is an element of the class. JFM CLASSES2 th. 2. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β π β§ π΄ βΊ π) β π΄ β π) | ||
Theorem | tskss 10776 | The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β π β§ π΅ β π΄) β π΅ β π) | ||
Theorem | tskin 10777 | The intersection of two elements of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β π) β (π΄ β© π΅) β π) | ||
Theorem | tsksn 10778 | A singleton of an element of a Tarski class belongs to the class. JFM CLASSES2 th. 2 (partly). (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β π) β {π΄} β π) | ||
Theorem | tsktrss 10779 | A transitive element of a Tarski class is a part of the class. JFM CLASSES2 th. 8. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ Tr π΄ β§ π΄ β π) β π΄ β π) | ||
Theorem | tsksuc 10780 | If an element of a Tarski class is an ordinal number, its successor is an element of the class. JFM CLASSES2 th. 6 (partly). (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π΄ β On β§ π΄ β π) β suc π΄ β π) | ||
Theorem | tsk0 10781 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β β β π) | ||
Theorem | tsk1 10782 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 1o β π) | ||
Theorem | tsk2 10783 | Two is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π β Tarski β§ π β β ) β 2o β π) | ||
Theorem | 2domtsk 10784 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 2o βΊ π) | ||
Theorem | tskr1om 10785 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9656.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β (π 1 β Ο) β π) | ||
Theorem | tskr1om2 10786 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9656.) (Contributed by NM, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β βͺ (π 1 β Ο) β π) | ||
Theorem | tskinf 10787 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β Ο βΌ π) | ||
Theorem | tskpr 10788 | If π΄ and π΅ are members of a Tarski class, their unordered pair is also an element of the class. JFM CLASSES2 th. 3 (partly). (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β π β§ π΅ β π) β {π΄, π΅} β π) | ||
Theorem | tskop 10789 | If π΄ and π΅ are members of a Tarski class, their ordered pair is also an element of the class. JFM CLASSES2 th. 4. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π΄ β π β§ π΅ β π) β β¨π΄, π΅β© β π) | ||
Theorem | tskxpss 10790 | A Cartesian product of two parts of a Tarski class is a part of the class. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β π β§ π΅ β π) β (π΄ Γ π΅) β π) | ||
Theorem | tskwe2 10791 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
β’ (π β Tarski β π β dom card) | ||
Theorem | inttsk 10792 | The intersection of a collection of Tarski classes is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ ((π΄ β Tarski β§ π΄ β β ) β β© π΄ β Tarski) | ||
Theorem | inar1 10793 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is equipotent to π΄. (Contributed by Mario Carneiro, 6-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β π΄) | ||
Theorem | r1omALT 10794 | Alternate proof of r1om 10262, shorter as a consequence of inar1 10793, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π 1βΟ) β Ο | ||
Theorem | rankcf 10795 | Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of π΄ form a cofinal map into (rankβπ΄). (Contributed by Mario Carneiro, 27-May-2013.) |
β’ Β¬ π΄ βΊ (cfβ(rankβπ΄)) | ||
Theorem | inatsk 10796 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β Tarski) | ||
Theorem | r1omtsk 10797 | The set of hereditarily finite sets is a Tarski class. (The Tarski-Grothendieck Axiom is not needed for this theorem.) (Contributed by Mario Carneiro, 28-May-2013.) |
β’ (π 1βΟ) β Tarski | ||
Theorem | tskord 10798 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β On β§ π΄ βΊ π) β π΄ β π) | ||
Theorem | tskcard 10799 | An even more direct relationship than r1tskina 10800 to get an inaccessible cardinal out of a Tarski class: the size of any nonempty Tarski class is an inaccessible cardinal. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β (cardβπ) β Inacc) | ||
Theorem | r1tskina 10800 | There is a direct relationship between transitive Tarski classes and inaccessible cardinals: the Tarski classes that occur in the cumulative hierarchy are exactly at the strongly inaccessible cardinals. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ (π΄ β On β ((π 1βπ΄) β Tarski β (π΄ = β β¨ π΄ β Inacc))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |