![]() |
Metamath
Proof Explorer Theorem List (p. 108 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elwina 10701* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inaccw β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | elina 10702* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (π΄ β Inacc β (π΄ β β β§ (cfβπ΄) = π΄ β§ βπ₯ β π΄ π« π₯ βΊ π΄)) | ||
Theorem | winaon 10703 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β π΄ β On) | ||
Theorem | inawinalem 10704* | Lemma for inawina 10705. (Contributed by Mario Carneiro, 8-Jun-2014.) |
β’ (π΄ β On β (βπ₯ β π΄ π« π₯ βΊ π΄ β βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) | ||
Theorem | inawina 10705 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inacc β π΄ β Inaccw) | ||
Theorem | omina 10706 | Ο 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 10707 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β (cardβπ΄) = π΄) | ||
Theorem | winainflem 10708* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β β β§ π΄ β On β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) β Ο β π΄) | ||
Theorem | winainf 10709 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Ο β π΄) | ||
Theorem | winalim 10710 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ (π΄ β Inaccw β Lim π΄) | ||
Theorem | winalim2 10711* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯)) | ||
Theorem | winafp 10712 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
β’ ((π΄ β Inaccw β§ π΄ β Ο) β (β΅βπ΄) = π΄) | ||
Theorem | winafpi 10713 | 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 4582 to turn this type of statement into the closed form statement winafp 10712, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10712 using this theorem and dedth 4582, in ZFC. (You can prove this if you use ax-groth 10838, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
β’ π΄ β Inaccw & β’ π΄ β Ο β β’ (β΅βπ΄) = π΄ | ||
Theorem | gchina 10714 | 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 10715 | Extend class definition to include the class of all weak universes. |
class WUni | ||
Syntax | cwunm 10716 | 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 10717* | 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 10755) whereas the analogue for Grothendieck universes requires ax-groth 10838 (see grothtsk 10850). (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ WUni = {π’ β£ (Tr π’ β§ π’ β β β§ βπ₯ β π’ (βͺ π₯ β π’ β§ π« π₯ β π’ β§ βπ¦ β π’ {π₯, π¦} β π’))} | ||
Definition | df-wunc 10718* | 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 10719* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β (π β WUni β (Tr π β§ π β β β§ βπ₯ β π (βͺ π₯ β π β§ π« π₯ β π β§ βπ¦ β π {π₯, π¦} β π)))) | ||
Theorem | wuntr 10720 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β WUni β Tr π) | ||
Theorem | wununi 10721 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β βͺ π΄ β π) | ||
Theorem | wunpw 10722 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | wunelss 10723 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π΄ β π) | ||
Theorem | wunpr 10724 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | wunun 10725 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | wuntp 10726 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β {π΄, π΅, πΆ} β π) | ||
Theorem | wunss 10727 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | wunin 10728 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β© π΅) β π) | ||
Theorem | wundif 10729 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wunint 10730 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ ((π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | wunsn 10731 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | wunsuc 10732 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β suc π΄ β π) | ||
Theorem | wun0 10733 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β β β π) | ||
Theorem | wunr1om 10734 | 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 10735 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β Ο β π) | ||
Theorem | wunfi 10736 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β π΄ β π) | ||
Theorem | wunop 10737 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β¨π΄, π΅β© β π) | ||
Theorem | wunot 10738 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β β¨π΄, π΅, πΆβ© β π) | ||
Theorem | wunxp 10739 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ Γ π΅) β π) | ||
Theorem | wunpm 10740 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βpm π΅) β π) | ||
Theorem | wunmap 10741 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βm π΅) β π) | ||
Theorem | wunf 10742 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β πΉ β π) | ||
Theorem | wundm 10743 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β dom π΄ β π) | ||
Theorem | wunrn 10744 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β ran π΄ β π) | ||
Theorem | wuncnv 10745 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β β‘π΄ β π) | ||
Theorem | wunres 10746 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ βΎ π΅) β π) | ||
Theorem | wunfv 10747 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄βπ΅) β π) | ||
Theorem | wunco 10748 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wuntpos 10749 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β tpos π΄ β π) | ||
Theorem | intwun 10750 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β WUni β§ π΄ β β ) β β© π΄ β WUni) | ||
Theorem | r1limwun 10751 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β π β§ Lim π΄) β (π 1βπ΄) β WUni) | ||
Theorem | r1wunlim 10752 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β ((π 1βπ΄) β WUni β Lim π΄)) | ||
Theorem | wunex2 10753* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) & β’ π = βͺ ran πΉ β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wunex 10754* | Construct a weak universe from a given set. See also wunex2 10753. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β βπ’ β WUni π΄ β π’) | ||
Theorem | uniwun 10755 | Every set is contained in a weak universe. This is the analogue of grothtsk 10850 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10850. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ βͺ WUni = V | ||
Theorem | wunex3 10756 | Construct a weak universe from a given set. This version of wunex 10754 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π = (π 1β((rankβπ΄) +o Ο)) β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wuncval 10757* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) = β© {π’ β WUni β£ π΄ β π’}) | ||
Theorem | wuncid 10758 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β π΄ β (wUniClβπ΄)) | ||
Theorem | wunccl 10759 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) β WUni) | ||
Theorem | wuncss 10760 | 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 10761 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβ(wUniClβπ΄)) = (wUniClβπ΄)) | ||
Theorem | wuncval2 10762* | 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 10763 | Extend class definition to include the class of all Tarski classes. |
class Tarski | ||
Definition | df-tsk 10764* | 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 10838 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 10765* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ βπ€ β π π« π§ β π€) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | eltsk2g 10766* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ π« π§ β π) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | tskpwss 10767 | 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 10768 | 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 10769 | 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 10770 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ β β Tarski | ||
Theorem | tsksdom 10771 | 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 10772 | 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 10773 | 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 10774 | 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 10775 | 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 10776 | 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 10777 | 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 10778 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β β β π) | ||
Theorem | tsk1 10779 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 1o β π) | ||
Theorem | tsk2 10780 | 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 10781 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 2o βΊ π) | ||
Theorem | tskr1om 10782 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9653.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β (π 1 β Ο) β π) | ||
Theorem | tskr1om2 10783 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9653.) (Contributed by NM, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β βͺ (π 1 β Ο) β π) | ||
Theorem | tskinf 10784 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β Ο βΌ π) | ||
Theorem | tskpr 10785 | 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 10786 | 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 10787 | 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 10788 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
β’ (π β Tarski β π β dom card) | ||
Theorem | inttsk 10789 | 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 10790 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is equipotent to π΄. (Contributed by Mario Carneiro, 6-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β π΄) | ||
Theorem | r1omALT 10791 | Alternate proof of r1om 10259, shorter as a consequence of inar1 10790, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π 1βΟ) β Ο | ||
Theorem | rankcf 10792 | 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 10793 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β Tarski) | ||
Theorem | r1omtsk 10794 | 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 10795 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β On β§ π΄ βΊ π) β π΄ β π) | ||
Theorem | tskcard 10796 | An even more direct relationship than r1tskina 10797 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 10797 | 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))) | ||
Theorem | tskuni 10798 | The union of an element of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ ((π β Tarski β§ Tr π β§ π΄ β π) β βͺ π΄ β π) | ||
Theorem | tskwun 10799 | A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π β Tarski β§ Tr π β§ π β β ) β π β WUni) | ||
Theorem | tskint 10800 | The intersection of an element of a transitive Tarski class is an element of the class. (Contributed by FL, 17-Apr-2011.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ (((π β Tarski β§ Tr π) β§ π΄ β π β§ π΄ β β ) β β© π΄ β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |