Home | Metamath
Proof Explorer Theorem List (p. 96 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gchhar 9501 | A "local" form of gchac 9503. If and are GCH-sets, then the Hartogs number of is (so and a fortiori are well-orderable). The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
GCH GCH har | ||
Theorem | gchacg 9502 | A "local" form of gchac 9503. If and are GCH-sets, then is well-orderable. The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH GCH | ||
Theorem | gchac 9503 | The Generalized Continuum Hypothesis implies the Axiom of Choice. The original proof is due to Sierpiński (1947); we use a refinement of Sierpiński's result due to Specker. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH CHOICE | ||
Here we introduce Tarski-Grothendieck (TG) set theory, named after mathematicians Alfred Tarski and Alexander Grothendieck. TG theory extends ZFC with the TG Axiom ax-groth 9645, which states that for every set there is an inaccessible cardinal such that is not in . The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics." We first introduce the concept of inaccessibles, including weakly and strongly inaccessible cardinals (df-wina 9506 and df-ina 9507 respectively ), Tarski classes (df-tsk 9571), and Grothendieck universes (df-gru 9613). We then introduce the Tarski's axiom ax-groth 9645 and prove various properties from that. | ||
Syntax | cwina 9504 | The class of weak inaccessibles. |
Syntax | cina 9505 | The class of strong inaccessibles. |
Definition | df-wina 9506* | 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.) |
Definition | df-ina 9507* | 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.) |
Theorem | elwina 9508* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
Theorem | elina 9509* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
Theorem | winaon 9510 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | inawinalem 9511* | Lemma for inawina 9512. (Contributed by Mario Carneiro, 8-Jun-2014.) |
Theorem | inawina 9512 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | omina 9513 | is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow as an inaccessible cardinal, but this choice allows us to reuse our results for inaccessibles for .) (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winacard 9514 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winainflem 9515* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winainf 9516 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winalim 9517 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winalim2 9518* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winafp 9519 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
Theorem | winafpi 9520 | 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 4139 to turn this type of statement into the closed form statement winafp 9519, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 9519 using this theorem and dedth 4139, in ZFC. (You can prove this if you use ax-groth 9645, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
Theorem | gchina 9521 | Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 5-Jun-2015.) |
GCH | ||
Syntax | cwun 9522 | Extend class definition to include the class of all weak universes. |
WUni | ||
Syntax | cwunm 9523 | Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset. |
wUniCl | ||
Definition | df-wun 9524* | 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 9562) whereas the analogue for Grothendieck universes requires ax-groth 9645 (see grothtsk 9657). (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Definition | df-wunc 9525* | 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 WUni | ||
Theorem | iswun 9526* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wuntr 9527 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wununi 9528 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunpw 9529 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunelss 9530 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunpr 9531 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunun 9532 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wuntp 9533 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunss 9534 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunin 9535 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wundif 9536 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunint 9537 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunsn 9538 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunsuc 9539 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wun0 9540 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunr1om 9541 | A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunom 9542 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunfi 9543 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunop 9544 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunot 9545 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunxp 9546 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunpm 9547 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunmap 9548 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunf 9549 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wundm 9550 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunrn 9551 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wuncnv 9552 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunres 9553 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
WUni | ||
Theorem | wunfv 9554 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
WUni | ||
Theorem | wunco 9555 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
WUni | ||
Theorem | wuntpos 9556 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
WUni tpos | ||
Theorem | intwun 9557 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni WUni | ||
Theorem | r1limwun 9558 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | r1wunlim 9559 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunex2 9560* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunex 9561* | Construct a weak universe from a given set. See also wunex2 9560. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | uniwun 9562 | Every set is contained in a weak universe. This is the analogue of grothtsk 9657 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 9657. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wunex3 9563 | Construct a weak universe from a given set. This version of wunex 9561 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
WUni | ||
Theorem | wuncval 9564* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
wUniCl WUni | ||
Theorem | wuncid 9565 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
wUniCl | ||
Theorem | wunccl 9566 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
wUniCl WUni | ||
Theorem | wuncss 9567 | 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 9568 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
wUniClwUniCl wUniCl | ||
Theorem | wuncval2 9569* | Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017.) |
wUniCl | ||
Syntax | ctsk 9570 | Extend class definition to include the class of all Tarski classes. |
Definition | df-tsk 9571* | 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 9645 and the equivalent axioms). Axiom A was first presented in Tarski's article _Über unerreichbare Kardinalzahlen_. Tarski introduced the axiom A to enable ZFC to manage inaccessible cardinals. Later Grothendieck introduced the concept of Grothendieck universes and showed they were equal to transitive Tarski classes. (Contributed by FL, 30-Dec-2010.) |
Theorem | eltskg 9572* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
Theorem | eltsk2g 9573* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
Theorem | tskpwss 9574 | 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.) |
Theorem | tskpw 9575 | 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.) |
Theorem | tsken 9576 | 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.) |
Theorem | 0tsk 9577 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
Theorem | tsksdom 9578 | 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.) |
Theorem | tskssel 9579 | 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.) |
Theorem | tskss 9580 | 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.) |
Theorem | tskin 9581 | 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.) |
Theorem | tsksn 9582 | 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.) |
Theorem | tsktrss 9583 | 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.) |
Theorem | tsksuc 9584 | 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.) |
Theorem | tsk0 9585 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
Theorem | tsk1 9586 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
Theorem | tsk2 9587 | Two is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
Theorem | 2domtsk 9588 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
Theorem | tskr1om 9589 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 8535.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
Theorem | tskr1om2 9590 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 8535.) (Contributed by NM, 22-Feb-2011.) |
Theorem | tskinf 9591 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
Theorem | tskpr 9592 | 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.) |
Theorem | tskop 9593 | 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.) |
Theorem | tskxpss 9594 | 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.) |
Theorem | tskwe2 9595 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
Theorem | inttsk 9596 | 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.) |
Theorem | inar1 9597 | for a strongly inaccessible cardinal is equipotent to . (Contributed by Mario Carneiro, 6-Jun-2013.) |
Theorem | r1omALT 9598 | Alternate proof of r1om 9066, shorter as a consequence of inar1 9597, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | rankcf 9599 | 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 . (Contributed by Mario Carneiro, 27-May-2013.) |
Theorem | inatsk 9600 | for a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |