| Mathbox for Eric Schmidt |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > wfaxext | Structured version Visualization version GIF version | ||
| Description: The class of well-founded
sets models the Axiom of Extensionality
ax-ext 2707. Part of Corollary II.2.5 of [Kunen2] p. 112.
This is the first of a series of theorems showing that all the axioms of ZFC hold in the class of well-founded sets, which we here denote by 𝑊. More precisely, for each axiom of ZFC, we obtain a provable statement if we restrict all quantifiers to 𝑊 (including implicit universal quantifiers on free variables). None of these proofs use the Axiom of Regularity. In particular, the Axiom of Regularity itself is proved to hold in 𝑊 without using Regularity. Further, the Axiom of Choice is used only in the proof that Choice holds in 𝑊. This has the consequence that any theorem of ZF (possibly proved using Regularity) can be proved, without using Regularity, to hold in 𝑊. This gives us a relative consistency result: If ZF without Regularity is consistent, so is ZF itself. Similarly, if ZFC without Regularity is consistent, so is ZFC itself. These consistency results are metatheorems and are part of Theorem II.2.13 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 11-Sep-2025.) (Revised by Eric Schmidt, 29-Sep-2025.) |
| Ref | Expression |
|---|---|
| wfax.1 | ⊢ 𝑊 = ∪ (𝑅1 “ On) |
| Ref | Expression |
|---|---|
| wfaxext | ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trwf 44954 | . . 3 ⊢ Tr ∪ (𝑅1 “ On) | |
| 2 | wfax.1 | . . . 4 ⊢ 𝑊 = ∪ (𝑅1 “ On) | |
| 3 | treq 5265 | . . . 4 ⊢ (𝑊 = ∪ (𝑅1 “ On) → (Tr 𝑊 ↔ Tr ∪ (𝑅1 “ On))) | |
| 4 | 2, 3 | ax-mp 5 | . . 3 ⊢ (Tr 𝑊 ↔ Tr ∪ (𝑅1 “ On)) |
| 5 | 1, 4 | mpbir 231 | . 2 ⊢ Tr 𝑊 |
| 6 | traxext 44970 | . 2 ⊢ (Tr 𝑊 → ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) | |
| 7 | 5, 6 | ax-mp 5 | 1 ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∀wral 3060 ∪ cuni 4905 Tr wtr 5257 “ cima 5686 Oncon0 6382 𝑅1cr1 9798 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-iun 4991 df-br 5142 df-opab 5204 df-mpt 5224 df-tr 5258 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6319 df-ord 6385 df-on 6386 df-lim 6387 df-suc 6388 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-ov 7432 df-om 7884 df-2nd 8011 df-frecs 8302 df-wrecs 8333 df-recs 8407 df-rdg 8446 df-r1 9800 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |