Home | Metamath
Proof Explorer Theorem List (p. 102 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gchacg 10101 | A "local" form of gchac 10102. 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) → 𝒫 𝐴 ∈ dom card) | ||
Theorem | gchac 10102 | 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 = V → 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 10244, 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 10105 and df-ina 10106 respectively ), Tarski classes (df-tsk 10170), and Grothendieck universes (df-gru 10212). We then introduce the Tarski's axiom ax-groth 10244 and prove various properties from that. | ||
Syntax | cwina 10103 | The class of weak inaccessibles. |
class Inaccw | ||
Syntax | cina 10104 | The class of strong inaccessibles. |
class Inacc | ||
Definition | df-wina 10105* | 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.) |
⊢ Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)} | ||
Definition | df-ina 10106* | 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.) |
⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} | ||
Theorem | elwina 10107* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
Theorem | elina 10108* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) | ||
Theorem | winaon 10109 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On) | ||
Theorem | inawinalem 10110* | Lemma for inawina 10111. (Contributed by Mario Carneiro, 8-Jun-2014.) |
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
Theorem | inawina 10111 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw) | ||
Theorem | omina 10112 | ω 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.) |
⊢ ω ∈ Inacc | ||
Theorem | winacard 10113 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴) | ||
Theorem | winainflem 10114* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) | ||
Theorem | winainf 10115 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴) | ||
Theorem | winalim 10116 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → Lim 𝐴) | ||
Theorem | winalim2 10117* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) | ||
Theorem | winafp 10118 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (ℵ‘𝐴) = 𝐴) | ||
Theorem | winafpi 10119 | 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 4522 to turn this type of statement into the closed form statement winafp 10118, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10118 using this theorem and dedth 4522, in ZFC. (You can prove this if you use ax-groth 10244, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ 𝐴 ∈ Inaccw & ⊢ 𝐴 ≠ ω ⇒ ⊢ (ℵ‘𝐴) = 𝐴 | ||
Theorem | gchina 10120 | 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 10121 | Extend class definition to include the class of all weak universes. |
class WUni | ||
Syntax | cwunm 10122 | 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 10123* | 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 10161) whereas the analogue for Grothendieck universes requires ax-groth 10244 (see grothtsk 10256). (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))} | ||
Definition | df-wunc 10124* | 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 10125* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))) | ||
Theorem | wuntr 10126 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝑈 ∈ WUni → Tr 𝑈) | ||
Theorem | wununi 10127 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | wunpw 10128 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
Theorem | wunelss 10129 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
Theorem | wunpr 10130 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | wunun 10131 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | wuntp 10132 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ 𝑈) | ||
Theorem | wunss 10133 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | wunin 10134 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝑈) | ||
Theorem | wundif 10135 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝑈) | ||
Theorem | wunint 10136 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑈) | ||
Theorem | wunsn 10137 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
Theorem | wunsuc 10138 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝑈) | ||
Theorem | wun0 10139 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
Theorem | wunr1om 10140 | 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 10141 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) ⇒ ⊢ (𝜑 → ω ⊆ 𝑈) | ||
Theorem | wunfi 10142 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
Theorem | wunop 10143 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑈) | ||
Theorem | wunot 10144 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵, 𝐶〉 ∈ 𝑈) | ||
Theorem | wunxp 10145 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ 𝑈) | ||
Theorem | wunpm 10146 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↑pm 𝐵) ∈ 𝑈) | ||
Theorem | wunmap 10147 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↑m 𝐵) ∈ 𝑈) | ||
Theorem | wunf 10148 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑈) | ||
Theorem | wundm 10149 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ 𝑈) | ||
Theorem | wunrn 10150 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ran 𝐴 ∈ 𝑈) | ||
Theorem | wuncnv 10151 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ◡𝐴 ∈ 𝑈) | ||
Theorem | wunres 10152 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ 𝑈) | ||
Theorem | wunfv 10153 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈) | ||
Theorem | wunco 10154 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈) | ||
Theorem | wuntpos 10155 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈) | ||
Theorem | intwun 10156 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni) | ||
Theorem | r1limwun 10157 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) | ||
Theorem | r1wunlim 10158 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴)) | ||
Theorem | wunex2 10159* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) & ⊢ 𝑈 = ∪ ran 𝐹 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
Theorem | wunex 10160* | Construct a weak universe from a given set. See also wunex2 10159. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢) | ||
Theorem | uniwun 10161 | Every set is contained in a weak universe. This is the analogue of grothtsk 10256 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10256. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ∪ WUni = V | ||
Theorem | wunex3 10162 | Construct a weak universe from a given set. This version of wunex 10160 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
Theorem | wuncval 10163* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢}) | ||
Theorem | wuncid 10164 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴)) | ||
Theorem | wunccl 10165 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni) | ||
Theorem | wuncss 10166 | 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 10167 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴)) | ||
Theorem | wuncval2 10168* | 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 10169 | Extend class definition to include the class of all Tarski classes. |
class Tarski | ||
Definition | df-tsk 10170* | 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 10244 and the equivalent axioms). Axiom A was first presented in Tarski's article Ueber 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.) |
⊢ Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))} | ||
Theorem | eltskg 10171* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
Theorem | eltsk2g 10172* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
Theorem | tskpwss 10173 | 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 10174 | 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 10175 | 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 10176 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
⊢ ∅ ∈ Tarski | ||
Theorem | tsksdom 10177 | 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 10178 | 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 10179 | 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 10180 | 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 10181 | 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 10182 | 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 10183 | 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 10184 | A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇) | ||
Theorem | tsk1 10185 | One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇) | ||
Theorem | tsk2 10186 | 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 10187 | If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇) | ||
Theorem | tskr1om 10188 | A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9100.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇) | ||
Theorem | tskr1om2 10189 | A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9100.) (Contributed by NM, 22-Feb-2011.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∪ (𝑅1 “ ω) ⊆ 𝑇) | ||
Theorem | tskinf 10190 | A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇) | ||
Theorem | tskpr 10191 | 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 10192 | 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 10193 | 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 10194 | A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.) |
⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card) | ||
Theorem | inttsk 10195 | 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 10196 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.) |
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴) | ||
Theorem | r1omALT 10197 | Alternate proof of r1om 9665, shorter as a consequence of inar1 10196, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑅1‘ω) ≈ ω | ||
Theorem | rankcf 10198 | 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 10199 | (𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski) | ||
Theorem | r1omtsk 10200 | 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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |