![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exmidpw2en | GIF version |
Description: The power set of a set
being equinumerous to set exponentiation with a
base of ordinal 2o is equivalent to
excluded middle. This is
Metamath 100 proof #52. The forward direction uses excluded middle
expressed as EXMID to show this
equinumerosity.
The reverse direction is the one which establishes that power set being equinumerous to set exponentiation implies excluded middle. This resolves the question of whether we will be able to prove this equinumerosity theorem in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.) |
Ref | Expression |
---|---|
exmidpw2en | ⊢ (EXMID ↔ ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vpwex 4208 | . . . . 5 ⊢ 𝒫 𝑥 ∈ V | |
2 | pp0ex 4218 | . . . . . . 7 ⊢ {∅, {∅}} ∈ V | |
3 | vex 2763 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
4 | 2, 3 | mapval 6709 | . . . . . 6 ⊢ ({∅, {∅}} ↑𝑚 𝑥) = {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}} |
5 | mapex 6703 | . . . . . . 7 ⊢ ((𝑥 ∈ V ∧ {∅, {∅}} ∈ V) → {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}} ∈ V) | |
6 | 3, 2, 5 | mp2an 426 | . . . . . 6 ⊢ {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}} ∈ V |
7 | 4, 6 | eqeltri 2266 | . . . . 5 ⊢ ({∅, {∅}} ↑𝑚 𝑥) ∈ V |
8 | 3 | a1i 9 | . . . . . 6 ⊢ (EXMID → 𝑥 ∈ V) |
9 | 0ex 4156 | . . . . . . 7 ⊢ ∅ ∈ V | |
10 | 9 | a1i 9 | . . . . . 6 ⊢ (EXMID → ∅ ∈ V) |
11 | p0ex 4217 | . . . . . . 7 ⊢ {∅} ∈ V | |
12 | 11 | a1i 9 | . . . . . 6 ⊢ (EXMID → {∅} ∈ V) |
13 | 0nep0 4194 | . . . . . . 7 ⊢ ∅ ≠ {∅} | |
14 | 13 | a1i 9 | . . . . . 6 ⊢ (EXMID → ∅ ≠ {∅}) |
15 | exmidexmid 4225 | . . . . . . . 8 ⊢ (EXMID → DECID 𝑝 ∈ 𝑞) | |
16 | 15 | ralrimivw 2568 | . . . . . . 7 ⊢ (EXMID → ∀𝑞 ∈ 𝒫 𝑥DECID 𝑝 ∈ 𝑞) |
17 | 16 | ralrimivw 2568 | . . . . . 6 ⊢ (EXMID → ∀𝑝 ∈ 𝑥 ∀𝑞 ∈ 𝒫 𝑥DECID 𝑝 ∈ 𝑞) |
18 | eqid 2193 | . . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))) = (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))) | |
19 | 8, 10, 12, 14, 17, 18 | pw2f1odc 6886 | . . . . 5 ⊢ (EXMID → (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))):𝒫 𝑥–1-1-onto→({∅, {∅}} ↑𝑚 𝑥)) |
20 | f1oen2g 6804 | . . . . 5 ⊢ ((𝒫 𝑥 ∈ V ∧ ({∅, {∅}} ↑𝑚 𝑥) ∈ V ∧ (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))):𝒫 𝑥–1-1-onto→({∅, {∅}} ↑𝑚 𝑥)) → 𝒫 𝑥 ≈ ({∅, {∅}} ↑𝑚 𝑥)) | |
21 | 1, 7, 19, 20 | mp3an12i 1352 | . . . 4 ⊢ (EXMID → 𝒫 𝑥 ≈ ({∅, {∅}} ↑𝑚 𝑥)) |
22 | df2o2 6479 | . . . . 5 ⊢ 2o = {∅, {∅}} | |
23 | 22 | oveq1i 5924 | . . . 4 ⊢ (2o ↑𝑚 𝑥) = ({∅, {∅}} ↑𝑚 𝑥) |
24 | 21, 23 | breqtrrdi 4071 | . . 3 ⊢ (EXMID → 𝒫 𝑥 ≈ (2o ↑𝑚 𝑥)) |
25 | 24 | alrimiv 1885 | . 2 ⊢ (EXMID → ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥)) |
26 | 1oex 6472 | . . . . 5 ⊢ 1o ∈ V | |
27 | pweq 3604 | . . . . . 6 ⊢ (𝑥 = 1o → 𝒫 𝑥 = 𝒫 1o) | |
28 | oveq2 5922 | . . . . . 6 ⊢ (𝑥 = 1o → (2o ↑𝑚 𝑥) = (2o ↑𝑚 1o)) | |
29 | 27, 28 | breq12d 4042 | . . . . 5 ⊢ (𝑥 = 1o → (𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) ↔ 𝒫 1o ≈ (2o ↑𝑚 1o))) |
30 | 26, 29 | spcv 2854 | . . . 4 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → 𝒫 1o ≈ (2o ↑𝑚 1o)) |
31 | df1o2 6477 | . . . . . 6 ⊢ 1o = {∅} | |
32 | 31 | oveq2i 5925 | . . . . 5 ⊢ (2o ↑𝑚 1o) = (2o ↑𝑚 {∅}) |
33 | 22, 2 | eqeltri 2266 | . . . . . 6 ⊢ 2o ∈ V |
34 | 33, 9 | mapsnen 6860 | . . . . 5 ⊢ (2o ↑𝑚 {∅}) ≈ 2o |
35 | 32, 34 | eqbrtri 4050 | . . . 4 ⊢ (2o ↑𝑚 1o) ≈ 2o |
36 | entr 6833 | . . . 4 ⊢ ((𝒫 1o ≈ (2o ↑𝑚 1o) ∧ (2o ↑𝑚 1o) ≈ 2o) → 𝒫 1o ≈ 2o) | |
37 | 30, 35, 36 | sylancl 413 | . . 3 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → 𝒫 1o ≈ 2o) |
38 | exmidpw 6959 | . . 3 ⊢ (EXMID ↔ 𝒫 1o ≈ 2o) | |
39 | 37, 38 | sylibr 134 | . 2 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → EXMID) |
40 | 25, 39 | impbii 126 | 1 ⊢ (EXMID ↔ ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 DECID wdc 835 ∀wal 1362 = wceq 1364 ∈ wcel 2164 {cab 2179 ≠ wne 2364 ∀wral 2472 Vcvv 2760 ∅c0 3446 ifcif 3557 𝒫 cpw 3601 {csn 3618 {cpr 3619 class class class wbr 4029 ↦ cmpt 4090 EXMIDwem 4223 ⟶wf 5246 –1-1-onto→wf1o 5249 (class class class)co 5914 1oc1o 6457 2oc2o 6458 ↑𝑚 cmap 6697 ≈ cen 6787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4462 ax-setind 4567 |
This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-exmid 4224 df-id 4322 df-iord 4395 df-on 4397 df-suc 4400 df-xp 4663 df-rel 4664 df-cnv 4665 df-co 4666 df-dm 4667 df-rn 4668 df-res 4669 df-ima 4670 df-iota 5211 df-fun 5252 df-fn 5253 df-f 5254 df-f1 5255 df-fo 5256 df-f1o 5257 df-fv 5258 df-ov 5917 df-oprab 5918 df-mpo 5919 df-1st 6188 df-2nd 6189 df-1o 6464 df-2o 6465 df-er 6582 df-map 6699 df-en 6790 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |