HomeTheorem List (p. 109 of 489)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 109 of 489) | < 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: | Metamath Proof Explorer
(1-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | wunfv 10801 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈) | ||
| Theorem | wunco 10802 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈) | ||
| Theorem | wuntpos 10803 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈) | ||
| Theorem | intwun 10804 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni) | ||
| Theorem | r1limwun 10805 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) | ||
| Theorem | r1wunlim 10806 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴)) | ||
| Theorem | wunex2 10807* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) & ⊢ 𝑈 = ∪ ran 𝐹 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
| Theorem | wunex 10808* | Construct a weak universe from a given set. See also wunex2 10807. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢) | ||
| Theorem | uniwun 10809 | Every set is contained in a weak universe. This is the analogue of grothtsk 10904 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10904. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ∪ WUni = V | ||
| Theorem | wunex3 10810 | Construct a weak universe from a given set. This version of wunex 10808 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
| Theorem | wuncval 10811* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢}) | ||
| Theorem | wuncid 10812 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴)) | ||
| Theorem | wunccl 10813 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni) | ||
| Theorem | wuncss 10814 | 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 10815 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴)) | ||
| Theorem | wuncval2 10816* | 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 10817 | Extend class definition to include the class of all Tarski classes. |
| class Tarski | ||
| Definition | df-tsk 10818* | 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 10892 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 10819* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
| ⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
| Theorem | eltsk2g 10820* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
| ⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
| Theorem | tskpwss 10821 | 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 10822 | 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 10823 | 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 10824 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
| ⊢ ∅ ∈ Tarski | ||
| Theorem | tsksdom 10825 | 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 10826 | 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 10827 | 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 10828 | 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 10829 | 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 10830 | 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 10831 | 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 10832 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇) | ||
| Theorem | tsk1 10833 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇) | ||
| Theorem | tsk2 10834 | 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 10835 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇) | ||
| Theorem | tskr1om 10836 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9707.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇) | ||
| Theorem | tskr1om2 10837 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9707.) (Contributed by NM, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∪ (𝑅1 “ ω) ⊆ 𝑇) | ||
| Theorem | tskinf 10838 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇) | ||
| Theorem | tskpr 10839 | 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 10840 | 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 10841 | 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 10842 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
| ⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card) | ||
| Theorem | inttsk 10843 | 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 10844 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.) |
| ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴) | ||
| Theorem | r1omALT 10845 | Alternate proof of r1om 10312, shorter as a consequence of inar1 10844, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑅1‘ω) ≈ ω | ||
| Theorem | rankcf 10846 | 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 10847 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski) | ||
| Theorem | r1omtsk 10848 | 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 10849 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇) | ||
| Theorem | tskcard 10850 | An even more direct relationship than r1tskina 10851 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 10851 | 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 10852 | 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 10853 | A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni) | ||
| Theorem | tskint 10854 | 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 10855 | 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 10856 | 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 10857 | 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 10858 | A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013.) |
| ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹:𝐴⟶𝑇) → ∪ ran 𝐹 ∈ 𝑇) | ||
| Syntax | cgru 10859 | Extend class notation to include the class of all Grothendieck universes. |
| class Univ | ||
| Definition | df-gru 10860* | 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 10861* | Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈)))) | ||
| Theorem | grutr 10862 | A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝑈 ∈ Univ → Tr 𝑈) | ||
| Theorem | gruelss 10863 | A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈) | ||
| Theorem | grupw 10864 | A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈) | ||
| Theorem | gruss 10865 | Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈) | ||
| Theorem | grupr 10866 | A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | gruurn 10867 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10868 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈) | ||
| Theorem | gruiun 10868* | 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 10869 | A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈) | ||
| Theorem | grurn 10870 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10868 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈) | ||
| Theorem | gruima 10871 | A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈)) | ||
| Theorem | gruel 10872 | 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 10873 | A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈) | ||
| Theorem | gruop 10874 | A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → ⟨𝐴, 𝐵⟩ ∈ 𝑈) | ||
| Theorem | gruun 10875 | A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
| Theorem | gruxp 10876 | A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈) | ||
| Theorem | grumap 10877 | A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈) | ||
| Theorem | gruixp 10878* | A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
| Theorem | gruiin 10879* | A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
| Theorem | gruf 10880 | A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈) | ||
| Theorem | gruen 10881 | 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 10882 | A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni) | ||
| Theorem | intgru 10883 | The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
| ⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ) | ||
| Theorem | ingru 10884* | 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 10885 | The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ) | ||
| Theorem | grudomon 10886 | 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 10887 | 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 10888 | A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.) |
| ⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈) | ||
| Theorem | grur1 10889 | A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.) |
| ⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴)) | ||
| Theorem | grutsk1 10890 | Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10852.) (Contributed by Mario Carneiro, 17-Jun-2013.) |
| ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ) | ||
| Theorem | grutsk 10891 | 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 10892* | 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 10903). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | axgroth5 10893* | The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) | ||
| Theorem | axgroth2 10894* | Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
| Theorem | grothpw 10895* | Derive the Axiom of Power Sets ax-pow 5383 from the Tarski-Grothendieck axiom ax-groth 10892. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10892. Note that ax-pow 5383 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
| ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
| Theorem | grothpwex 10896 | Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10892. Note that ax-pow 5383 is not used by the proof. Use axpweq 5369 to obtain ax-pow 5383. Use pwex 5398 or pwexg 5396 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
| ⊢ 𝒫 𝑥 ∈ V | ||
| Theorem | axgroth6 10897* | 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 10898 | The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9712). 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 10899 | The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10538). This can be put in a more conventional form via ween 10104 and dfac8 10205. 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 10205). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
| ⊢ dom card = V | ||
| Theorem | axgroth3 10900* | Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10504 is used to derive this version. (Contributed by NM, 26-Mar-2007.) |
| ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |