| Metamath
Proof Explorer Theorem List (p. 108 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 | pwfseqlem4a 10701* | Lemma for pwfseqlem4 10702. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) | ||
| Theorem | pwfseqlem4 10702* | Lemma for pwfseq 10704. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10700. Applying fpwwe2 10683 to it, we get a certain maximal well-ordered subset 𝑍, but the defining property (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 contradicts our assumption on 𝐹, so we are reduced to the case of 𝑍 finite. This too is a contradiction, though, because 𝑍 and its preimage under (𝑊‘𝑍) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by Matthew House, 10-Sep-2025.) |
| ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) & ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))} & ⊢ 𝑍 = ∪ dom 𝑊 ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | pwfseqlem5 10703* |
Lemma for pwfseq 10704. Although in some ways pwfseqlem4 10702 is the "main"
part of the proof, one last aspect which makes up a remark in the
original text is by far the hardest part to formalize. The main proof
relies on the existence of an injection 𝐾 from the set of finite
sequences on an infinite set 𝑥 to 𝑥. Now this alone would
not
be difficult to prove; this is mostly the claim of fseqen 10067. However,
what is needed for the proof is a canonical injection on these
sets,
so we have to start from scratch pulling together explicit bijections
from the lemmas.
If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 10054. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 9746), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10058). (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) & ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) & ⊢ 𝑂 = OrdIso(𝑟, 𝑡) & ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) & ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) & ⊢ 𝑆 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) & ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) & ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) & ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | pwfseq 10704* | The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of [KanamoriPincus] p. 418. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) | ||
| Theorem | pwxpndom2 10705 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 18-Jul-2022.) |
| ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴))) | ||
| Theorem | pwxpndom 10706 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 × 𝐴)) | ||
| Theorem | pwdjundom 10707 | The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ 𝐴)) | ||
| Theorem | gchdjuidm 10708 | An infinite GCH-set is idempotent under cardinal sum. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴) | ||
| Theorem | gchxpidm 10709 | An infinite GCH-set is idempotent under cardinal product. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) | ||
| Theorem | gchpwdom 10710 | A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of [KanamoriPincus] p. 421. (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴 ≺ 𝐵 ↔ 𝒫 𝐴 ≼ 𝐵)) | ||
| Theorem | gchaleph 10711 | If (ℵ‘𝐴) is a GCH-set and its powerset is well-orderable, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) | ||
| Theorem | gchaleph2 10712 | If (ℵ‘𝐴) and (ℵ‘suc 𝐴) are GCH-sets, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 31-May-2015.) |
| ⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ (ℵ‘suc 𝐴) ∈ GCH) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) | ||
| Theorem | hargch 10713 | If 𝐴 + ≈ 𝒫 𝐴, then 𝐴 is a GCH-set. The much simpler converse to gchhar 10719. (Contributed by Mario Carneiro, 2-Jun-2015.) |
| ⊢ ((har‘𝐴) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH) | ||
| Theorem | alephgch 10714 | If (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴), then (ℵ‘𝐴) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ ((ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ GCH) | ||
| Theorem | gch2 10715 | It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (GCH = V ↔ ran ℵ ⊆ GCH) | ||
| Theorem | gch3 10716 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (GCH = V ↔ ∀𝑥 ∈ On (ℵ‘suc 𝑥) ≈ 𝒫 (ℵ‘𝑥)) | ||
| Theorem | gch-kn 10717* | The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets", available at http://www.e-atheneum.net/science/derivation_ch.pdf. The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf. The key idea in the proof below is to equate both sides of alephexp2 10621 to the successor aleph using enen2 9158. (Contributed by NM, 1-Oct-2004.) |
| ⊢ (𝐴 ∈ On → ((ℵ‘suc 𝐴) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))} ↔ (ℵ‘suc 𝐴) ≈ (2o ↑m (ℵ‘𝐴)))) | ||
| Theorem | gchaclem 10718 | Lemma for gchac 10721 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (𝜑 → ω ≼ 𝐴) & ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH) & ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) ⇒ ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) | ||
| Theorem | gchhar 10719 | A "local" form of gchac 10721. 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 10720 | A "local" form of gchac 10721. 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 10721 | 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 10863, 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 10724 and df-ina 10725 respectively ), Tarski classes (df-tsk 10789), and Grothendieck universes (df-gru 10831). We then introduce the Tarski's axiom ax-groth 10863 and prove various properties from that. | ||
| Syntax | cwina 10722 | The class of weak inaccessibles. |
| class Inaccw | ||
| Syntax | cina 10723 | The class of strong inaccessibles. |
| class Inacc | ||
| Definition | df-wina 10724* | 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 10725* | 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 10726* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
| ⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
| Theorem | elina 10727* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
| ⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) | ||
| Theorem | winaon 10728 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On) | ||
| Theorem | inawinalem 10729* | Lemma for inawina 10730. (Contributed by Mario Carneiro, 8-Jun-2014.) |
| ⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
| Theorem | inawina 10730 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw) | ||
| Theorem | omina 10731 | ω is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow ω as an inaccessible cardinal, but this choice allows to reuse our results for inaccessibles for ω.) (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ ω ∈ Inacc | ||
| Theorem | winacard 10732 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴) | ||
| Theorem | winainflem 10733* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) | ||
| Theorem | winainf 10734 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴) | ||
| Theorem | winalim 10735 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ (𝐴 ∈ Inaccw → Lim 𝐴) | ||
| Theorem | winalim2 10736* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) | ||
| Theorem | winafp 10737 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
| ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (ℵ‘𝐴) = 𝐴) | ||
| Theorem | winafpi 10738 | 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 4584 to turn this type of statement into the closed form statement winafp 10737, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10737 using this theorem and dedth 4584, in ZFC. (You can prove this if you use ax-groth 10863, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
| ⊢ 𝐴 ∈ Inaccw & ⊢ 𝐴 ≠ ω ⇒ ⊢ (ℵ‘𝐴) = 𝐴 | ||
| Theorem | gchina 10739 | 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 10740 | Extend class definition to include the class of all weak universes. |
| class WUni | ||
| Syntax | cwunm 10741 | 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 10742* | 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 10780) whereas the analogue for Grothendieck universes requires ax-groth 10863 (see grothtsk 10875). (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))} | ||
| Definition | df-wunc 10743* | 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 10744* | Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))) | ||
| Theorem | wuntr 10745 | A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝑈 ∈ WUni → Tr 𝑈) | ||
| Theorem | wununi 10746 | A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
| Theorem | wunpw 10747 | A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
| Theorem | wunelss 10748 | The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑈) | ||
| Theorem | wunpr 10749 | A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | wunun 10750 | A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
| Theorem | wuntp 10751 | A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ 𝑈) | ||
| Theorem | wunss 10752 | A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
| Theorem | wunin 10753 | A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝑈) | ||
| Theorem | wundif 10754 | A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝑈) | ||
| Theorem | wunint 10755 | A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑈) | ||
| Theorem | wunsn 10756 | A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
| Theorem | wunsuc 10757 | A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝑈) | ||
| Theorem | wun0 10758 | A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
| Theorem | wunr1om 10759 | 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 10760 | A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) ⇒ ⊢ (𝜑 → ω ⊆ 𝑈) | ||
| Theorem | wunfi 10761 | A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
| Theorem | wunop 10762 | A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑈) | ||
| Theorem | wunot 10763 | A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵, 𝐶〉 ∈ 𝑈) | ||
| Theorem | wunxp 10764 | A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ 𝑈) | ||
| Theorem | wunpm 10765 | A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↑pm 𝐵) ∈ 𝑈) | ||
| Theorem | wunmap 10766 | A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↑m 𝐵) ∈ 𝑈) | ||
| Theorem | wunf 10767 | A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑈) | ||
| Theorem | wundm 10768 | A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → dom 𝐴 ∈ 𝑈) | ||
| Theorem | wunrn 10769 | A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ran 𝐴 ∈ 𝑈) | ||
| Theorem | wuncnv 10770 | A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ◡𝐴 ∈ 𝑈) | ||
| Theorem | wunres 10771 | A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ 𝑈) | ||
| Theorem | wunfv 10772 | A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈) | ||
| Theorem | wunco 10773 | A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈) | ||
| Theorem | wuntpos 10774 | A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈) | ||
| Theorem | intwun 10775 | The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni) | ||
| Theorem | r1limwun 10776 | Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni) | ||
| Theorem | r1wunlim 10777 | The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴)) | ||
| Theorem | wunex2 10778* | Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) & ⊢ 𝑈 = ∪ ran 𝐹 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
| Theorem | wunex 10779* | Construct a weak universe from a given set. See also wunex2 10778. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢) | ||
| Theorem | uniwun 10780 | Every set is contained in a weak universe. This is the analogue of grothtsk 10875 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10875. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ ∪ WUni = V | ||
| Theorem | wunex3 10781 | Construct a weak universe from a given set. This version of wunex 10779 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) | ||
| Theorem | wuncval 10782* | Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢}) | ||
| Theorem | wuncid 10783 | The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴)) | ||
| Theorem | wunccl 10784 | The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni) | ||
| Theorem | wuncss 10785 | 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 10786 | The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴)) | ||
| Theorem | wuncval2 10787* | 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 10788 | Extend class definition to include the class of all Tarski classes. |
| class Tarski | ||
| Definition | df-tsk 10789* | 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 10863 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 10790* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) |
| ⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
| Theorem | eltsk2g 10791* | Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
| ⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇)))) | ||
| Theorem | tskpwss 10792 | 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 10793 | 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 10794 | 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 10795 | The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.) |
| ⊢ ∅ ∈ Tarski | ||
| Theorem | tsksdom 10796 | 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 10797 | 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 10798 | 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 10799 | 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 10800 | 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 ∧ 𝐴 ∈ 𝑇) → {𝐴} ∈ 𝑇) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |