| Metamath
Proof Explorer Theorem List (p. 109 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tsktrss 10801 | 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 10802 | 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 10803 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇) | ||
| Theorem | tsk1 10804 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇) | ||
| Theorem | tsk2 10805 | 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 10806 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇) | ||
| Theorem | tskr1om 10807 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9678.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇) | ||
| Theorem | tskr1om2 10808 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9678.) (Contributed by NM, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∪ (𝑅1 “ ω) ⊆ 𝑇) | ||
| Theorem | tskinf 10809 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇) | ||
| Theorem | tskpr 10810 | 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 10811 | 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 10812 | 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 10813 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
| ⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card) | ||
| Theorem | inttsk 10814 | 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 10815 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.) |
| ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴) | ||
| Theorem | r1omALT 10816 | Alternate proof of r1om 10283, shorter as a consequence of inar1 10815, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑅1‘ω) ≈ ω | ||
| Theorem | rankcf 10817 | 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 10818 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski) | ||
| Theorem | r1omtsk 10819 | 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 10820 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇) | ||
| Theorem | tskcard 10821 | An even more direct relationship than r1tskina 10822 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 10822 | 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 10823 | 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 10824 | A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni) | ||
| Theorem | tskint 10825 | 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 10826 | 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 10827 | 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 10828 | 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 10829 | A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013.) |
| ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹:𝐴⟶𝑇) → ∪ ran 𝐹 ∈ 𝑇) | ||
| Syntax | cgru 10830 | Extend class notation to include the class of all Grothendieck universes. |
| class Univ | ||
| Definition | df-gru 10831* | 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 10832* | Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈)))) | ||
| Theorem | grutr 10833 | A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝑈 ∈ Univ → Tr 𝑈) | ||
| Theorem | gruelss 10834 | A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈) | ||
| Theorem | grupw 10835 | A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈) | ||
| Theorem | gruss 10836 | Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈) | ||
| Theorem | grupr 10837 | A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | gruurn 10838 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10839 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈) | ||
| Theorem | gruiun 10839* | 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 10840 | A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈) | ||
| Theorem | grurn 10841 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10839 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈) | ||
| Theorem | gruima 10842 | A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈)) | ||
| Theorem | gruel 10843 | 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 10844 | A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈) | ||
| Theorem | gruop 10845 | A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → 〈𝐴, 𝐵〉 ∈ 𝑈) | ||
| Theorem | gruun 10846 | A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
| Theorem | gruxp 10847 | A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈) | ||
| Theorem | grumap 10848 | A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈) | ||
| Theorem | gruixp 10849* | A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
| Theorem | gruiin 10850* | A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
| Theorem | gruf 10851 | A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈) | ||
| Theorem | gruen 10852 | A Grothendieck universe contains all subsets of itself that are equipotent to an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ (𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴)) → 𝐴 ∈ 𝑈) | ||
| Theorem | gruwun 10853 | A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni) | ||
| Theorem | intgru 10854 | The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ) | ||
| Theorem | ingru 10855* | The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran 𝑦 ∈ 𝐴))) → (𝑈 ∈ Univ → (𝑈 ∩ 𝐴) ∈ Univ)) | ||
| Theorem | wfgru 10856 | The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ) | ||
| Theorem | grudomon 10857 | Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵)) → 𝐴 ∈ 𝑈) | ||
| Theorem | gruina 10858 | If a Grothendieck universe 𝑈 is nonempty, then the height of the ordinals in 𝑈 is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) | ||
| Theorem | grur1a 10859 | A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.) |
| ⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈) | ||
| Theorem | grur1 10860 | A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.) |
| ⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴)) | ||
| Theorem | grutsk1 10861 | Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10823.) (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ) | ||
| Theorem | grutsk 10862 | Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
| ⊢ Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥} | ||
| Axiom | ax-groth 10863* | The Tarski-Grothendieck Axiom. 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". This version of the axiom is used by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html). Unlike the ZFC axioms, this axiom is very long when expressed in terms of primitive symbols (see grothprim 10874). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | axgroth5 10864* | The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) | ||
| Theorem | axgroth2 10865* | Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | grothpw 10866* | Derive the Axiom of Power Sets ax-pow 5365 from the Tarski-Grothendieck axiom ax-groth 10863. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10863. Note that ax-pow 5365 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
| ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
| Theorem | grothpwex 10867 | Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10863. Note that ax-pow 5365 is not used by the proof. Use axpweq 5351 to obtain ax-pow 5365. Use pwex 5380 or pwexg 5378 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
| ⊢ 𝒫 𝑥 ∈ V | ||
| Theorem | axgroth6 10868* | The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set 𝑥, there exists a set 𝑦 containing 𝑥, the subsets of the members of 𝑦, the power sets of the members of 𝑦, and the subsets of 𝑦 of cardinality less than that of 𝑦. (Contributed by NM, 21-Jun-2009.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) | ||
| Theorem | grothomex 10869 | The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9683). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
| ⊢ ω ∈ V | ||
| Theorem | grothac 10870 | The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10509). This can be put in a more conventional form via ween 10075 and dfac8 10176. Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10176). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
| ⊢ dom card = V | ||
| Theorem | axgroth3 10871* | Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10475 is used to derive this version. (Contributed by NM, 26-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | axgroth4 10872* | Alternate version of the Tarski-Grothendieck Axiom. ax-ac 10499 is used to derive this version. (Contributed by NM, 16-Apr-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | grothprimlem 10873* | Lemma for grothprim 10874. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.) |
| ⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) | ||
| Theorem | grothprim 10874* | The Tarski-Grothendieck Axiom ax-groth 10863 expanded into set theory primitives using 163 symbols (allowing the defined symbols ∧, ∨, ↔, and ∃). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) | ||
| Theorem | grothtsk 10875 | The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.) |
| ⊢ ∪ Tarski = V | ||
| Theorem | inaprc 10876 | An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ Inacc ∉ V | ||
| Syntax | ctskm 10877 | Extend class definition to include the map whose value is the smallest Tarski class. |
| class tarskiMap | ||
| Definition | df-tskm 10878* | A function that maps a set 𝑥 to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.) |
| ⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}) | ||
| Theorem | tskmval 10879* | Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥}) | ||
| Theorem | tskmid 10880 | The set 𝐴 is an element of the smallest Tarski class that contains 𝐴. CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (tarskiMap‘𝐴)) | ||
| Theorem | tskmcl 10881 | A Tarski class that contains 𝐴 is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
| ⊢ (tarskiMap‘𝐴) ∈ Tarski | ||
| Theorem | sstskm 10882* | Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥))) | ||
| Theorem | eltskm 10883* | Belonging to (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ∈ 𝑥))) | ||
This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 11212). After that, we derive their basic properties, various operations like addition (df-add 11166) and sine (df-sin 16105), and subsets such as the integers (df-z 12614) and natural numbers (df-nn 12267). | ||
| Syntax | cnpi 10884 |
The set of positive integers, which is the set of natural numbers ω
with 0 removed.
Note: This is the start of the Dedekind-cut construction of real and complex numbers. The last lemma of the construction is mulcnsrec 11184. The actual set of Dedekind cuts is defined by df-np 11021. |
| class N | ||
| Syntax | cpli 10885 | Positive integer addition. |
| class +N | ||
| Syntax | cmi 10886 | Positive integer multiplication. |
| class ·N | ||
| Syntax | clti 10887 | Positive integer ordering relation. |
| class <N | ||
| Syntax | cplpq 10888 | Positive pre-fraction addition. |
| class +pQ | ||
| Syntax | cmpq 10889 | Positive pre-fraction multiplication. |
| class ·pQ | ||
| Syntax | cltpq 10890 | Positive pre-fraction ordering relation. |
| class <pQ | ||
| Syntax | ceq 10891 | Equivalence class used to construct positive fractions. |
| class ~Q | ||
| Syntax | cnq 10892 | Set of positive fractions. |
| class Q | ||
| Syntax | c1q 10893 | The positive fraction constant 1. |
| class 1Q | ||
| Syntax | cerq 10894 | Positive fraction equivalence class. |
| class [Q] | ||
| Syntax | cplq 10895 | Positive fraction addition. |
| class +Q | ||
| Syntax | cmq 10896 | Positive fraction multiplication. |
| class ·Q | ||
| Syntax | crq 10897 | Positive fraction reciprocal operation. |
| class *Q | ||
| Syntax | cltq 10898 | Positive fraction ordering relation. |
| class <Q | ||
| Syntax | cnp 10899 | Set of positive reals. |
| class P | ||
| Syntax | c1p 10900 | Positive real constant 1. |
| class 1P | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |