![]() |
Metamath
Proof Explorer Theorem List (p. 108 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wunpw 10701 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | wunelss 10702 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β π΄ β π) | ||
Theorem | wunpr 10703 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | wunun 10704 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | wuntp 10705 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β {π΄, π΅, πΆ} β π) | ||
Theorem | wunss 10706 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | wunin 10707 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β© π΅) β π) | ||
Theorem | wundif 10708 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wunint 10709 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ ((π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | wunsn 10710 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | wunsuc 10711 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β suc π΄ β π) | ||
Theorem | wun0 10712 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β β β π) | ||
Theorem | wunr1om 10713 | 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 10714 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) β β’ (π β Ο β π) | ||
Theorem | wunfi 10715 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β π΄ β π) | ||
Theorem | wunop 10716 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β¨π΄, π΅β© β π) | ||
Theorem | wunot 10717 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β β¨π΄, π΅, πΆβ© β π) | ||
Theorem | wunxp 10718 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ Γ π΅) β π) | ||
Theorem | wunpm 10719 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βpm π΅) β π) | ||
Theorem | wunmap 10720 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βm π΅) β π) | ||
Theorem | wunf 10721 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β πΉ β π) | ||
Theorem | wundm 10722 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β dom π΄ β π) | ||
Theorem | wunrn 10723 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β ran π΄ β π) | ||
Theorem | wuncnv 10724 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β β‘π΄ β π) | ||
Theorem | wunres 10725 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄ βΎ π΅) β π) | ||
Theorem | wunfv 10726 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β (π΄βπ΅) β π) | ||
Theorem | wunco 10727 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ β π΅) β π) | ||
Theorem | wuntpos 10728 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β π΄ β π) β β’ (π β tpos π΄ β π) | ||
Theorem | intwun 10729 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β WUni β§ π΄ β β ) β β© π΄ β WUni) | ||
Theorem | r1limwun 10730 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π΄ β π β§ Lim π΄) β (π 1βπ΄) β WUni) | ||
Theorem | r1wunlim 10731 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β ((π 1βπ΄) β WUni β Lim π΄)) | ||
Theorem | wunex2 10732* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ πΉ = (rec((π§ β V β¦ ((π§ βͺ βͺ π§) βͺ βͺ π₯ β π§ ({π« π₯, βͺ π₯} βͺ ran (π¦ β π§ β¦ {π₯, π¦})))), (π΄ βͺ 1o)) βΎ Ο) & β’ π = βͺ ran πΉ β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wunex 10733* | Construct a weak universe from a given set. See also wunex2 10732. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β βπ’ β WUni π΄ β π’) | ||
Theorem | uniwun 10734 | Every set is contained in a weak universe. This is the analogue of grothtsk 10829 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10829. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ βͺ WUni = V | ||
Theorem | wunex3 10735 | Construct a weak universe from a given set. This version of wunex 10733 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ π = (π 1β((rankβπ΄) +o Ο)) β β’ (π΄ β π β (π β WUni β§ π΄ β π)) | ||
Theorem | wuncval 10736* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) = β© {π’ β WUni β£ π΄ β π’}) | ||
Theorem | wuncid 10737 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β π΄ β (wUniClβπ΄)) | ||
Theorem | wunccl 10738 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβπ΄) β WUni) | ||
Theorem | wuncss 10739 | 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 10740 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π΄ β π β (wUniClβ(wUniClβπ΄)) = (wUniClβπ΄)) | ||
Theorem | wuncval2 10741* | 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 10742 | Extend class definition to include the class of all Tarski classes. |
class Tarski | ||
Definition | df-tsk 10743* | 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 10817 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 10744* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ βπ€ β π π« π§ β π€) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | eltsk2g 10745* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
β’ (π β π β (π β Tarski β (βπ§ β π (π« π§ β π β§ π« π§ β π) β§ βπ§ β π« π(π§ β π β¨ π§ β π)))) | ||
Theorem | tskpwss 10746 | 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 10747 | 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 10748 | 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 10749 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
β’ β β Tarski | ||
Theorem | tsksdom 10750 | 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 10751 | 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 10752 | 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 10753 | 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 10754 | 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 10755 | 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 10756 | 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 10757 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β β β π) | ||
Theorem | tsk1 10758 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 1o β π) | ||
Theorem | tsk2 10759 | 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 10760 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β 2o βΊ π) | ||
Theorem | tskr1om 10761 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9632.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
β’ ((π β Tarski β§ π β β ) β (π 1 β Ο) β π) | ||
Theorem | tskr1om2 10762 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9632.) (Contributed by NM, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β βͺ (π 1 β Ο) β π) | ||
Theorem | tskinf 10763 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
β’ ((π β Tarski β§ π β β ) β Ο βΌ π) | ||
Theorem | tskpr 10764 | 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 10765 | 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 10766 | 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 10767 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
β’ (π β Tarski β π β dom card) | ||
Theorem | inttsk 10768 | 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 10769 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is equipotent to π΄. (Contributed by Mario Carneiro, 6-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β π΄) | ||
Theorem | r1omALT 10770 | Alternate proof of r1om 10238, shorter as a consequence of inar1 10769, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π 1βΟ) β Ο | ||
Theorem | rankcf 10771 | 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 10772 | (π 1βπ΄) for π΄ a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ (π΄ β Inacc β (π 1βπ΄) β Tarski) | ||
Theorem | r1omtsk 10773 | 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 10774 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
β’ ((π β Tarski β§ π΄ β On β§ π΄ βΊ π) β π΄ β π) | ||
Theorem | tskcard 10775 | An even more direct relationship than r1tskina 10776 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 10776 | 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 10777 | 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 10778 | A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ ((π β Tarski β§ Tr π β§ π β β ) β π β WUni) | ||
Theorem | tskint 10779 | 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 π) β§ π΄ β π β§ π΄ β β ) β β© π΄ β π) | ||
Theorem | tskun 10780 | The union of two elements of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 20-Sep-2014.) |
β’ (((π β Tarski β§ Tr π) β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) | ||
Theorem | tskxp 10781 | The Cartesian product of two elements of a transitive Tarski class is an element of the class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ (((π β Tarski β§ Tr π) β§ π΄ β π β§ π΅ β π) β (π΄ Γ π΅) β π) | ||
Theorem | tskmap 10782 | Set exponentiation is an element of a transitive Tarski class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
β’ (((π β Tarski β§ Tr π) β§ π΄ β π β§ π΅ β π) β (π΄ βm π΅) β π) | ||
Theorem | tskurn 10783 | A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013.) |
β’ (((π β Tarski β§ Tr π) β§ π΄ β π β§ πΉ:π΄βΆπ) β βͺ ran πΉ β π) | ||
Syntax | cgru 10784 | Extend class notation to include the class of all Grothendieck universes. |
class Univ | ||
Definition | df-gru 10785* | A Grothendieck universe is a set that is closed with respect to all the operations that are common in set theory: pairs, powersets, unions, intersections, Cartesian products etc. Grothendieck and alii, SΓ©minaire de GΓ©omΓ©trie AlgΓ©brique 4, ExposΓ© I, p. 185. It was designed to give a precise meaning to the concepts of categories of sets, groups... (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ Univ = {π’ β£ (Tr π’ β§ βπ₯ β π’ (π« π₯ β π’ β§ βπ¦ β π’ {π₯, π¦} β π’ β§ βπ¦ β (π’ βm π₯)βͺ ran π¦ β π’))} | ||
Theorem | elgrug 10786* | Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ (π β π β (π β Univ β (Tr π β§ βπ₯ β π (π« π₯ β π β§ βπ¦ β π {π₯, π¦} β π β§ βπ¦ β (π βm π₯)βͺ ran π¦ β π)))) | ||
Theorem | grutr 10787 | A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
β’ (π β Univ β Tr π) | ||
Theorem | gruelss 10788 | A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π) β π΄ β π) | ||
Theorem | grupw 10789 | A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π) β π« π΄ β π) | ||
Theorem | gruss 10790 | Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ π΅ β π΄) β π΅ β π) | ||
Theorem | grupr 10791 | A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ π΅ β π) β {π΄, π΅} β π) | ||
Theorem | gruurn 10792 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10793 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ πΉ:π΄βΆπ) β βͺ ran πΉ β π) | ||
Theorem | gruiun 10793* | If π΅(π₯) is a family of elements of π and the index set π΄ is an element of π, then the indexed union βͺ π₯ β π΄π΅ is also an element of π, where π is a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ βπ₯ β π΄ π΅ β π) β βͺ π₯ β π΄ π΅ β π) | ||
Theorem | gruuni 10794 | A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π) β βͺ π΄ β π) | ||
Theorem | grurn 10795 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10793 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ πΉ:π΄βΆπ) β ran πΉ β π) | ||
Theorem | gruima 10796 | A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ Fun πΉ β§ (πΉ β π΄) β π) β (π΄ β π β (πΉ β π΄) β π)) | ||
Theorem | gruel 10797 | Any element of an element of a Grothendieck universe is also an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ π΅ β π΄) β π΅ β π) | ||
Theorem | grusn 10798 | A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π) β {π΄} β π) | ||
Theorem | gruop 10799 | A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ π΅ β π) β β¨π΄, π΅β© β π) | ||
Theorem | gruun 10800 | A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
β’ ((π β Univ β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |