Theorem exmidpw2en 7042

Description: The power set of a set being equinumerous to set exponentiation with a base of ordinal 2_o 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.)

Assertion

Ref	Expression
exmidpw2en	⊢ (EXMID ↔ ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥))

Proof of Theorem exmidpw2en

Dummy variables 𝑓 𝑝 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vpwex 4242	. . . . 5 ⊢ 𝒫 𝑥 ∈ V
2		pp0ex 4252	. . . . . . 7 ⊢ {∅, {∅}} ∈ V
3		vex 2782	. . . . . . 7 ⊢ 𝑥 ∈ V
4	2, 3	mapval 6777	. . . . . 6 ⊢ ({∅, {∅}} ↑𝑚 𝑥) = {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}}
5		mapex 6771	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ {∅, {∅}} ∈ V) → {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}} ∈ V)
6	3, 2, 5	mp2an 426	. . . . . 6 ⊢ {𝑓 ∣ 𝑓:𝑥⟶{∅, {∅}}} ∈ V
7	4, 6	eqeltri 2282	. . . . 5 ⊢ ({∅, {∅}} ↑𝑚 𝑥) ∈ V
8	3	a1i 9	. . . . . 6 ⊢ (EXMID → 𝑥 ∈ V)
9		0ex 4190	. . . . . . 7 ⊢ ∅ ∈ V
10	9	a1i 9	. . . . . 6 ⊢ (EXMID → ∅ ∈ V)
11		p0ex 4251	. . . . . . 7 ⊢ {∅} ∈ V
12	11	a1i 9	. . . . . 6 ⊢ (EXMID → {∅} ∈ V)
13		0nep0 4228	. . . . . . 7 ⊢ ∅ ≠ {∅}
14	13	a1i 9	. . . . . 6 ⊢ (EXMID → ∅ ≠ {∅})
15		exmidexmid 4259	. . . . . . . 8 ⊢ (EXMID → DECID 𝑝 ∈ 𝑞)
16	15	ralrimivw 2584	. . . . . . 7 ⊢ (EXMID → ∀𝑞 ∈ 𝒫 𝑥DECID 𝑝 ∈ 𝑞)
17	16	ralrimivw 2584	. . . . . 6 ⊢ (EXMID → ∀𝑝 ∈ 𝑥 ∀𝑞 ∈ 𝒫 𝑥DECID 𝑝 ∈ 𝑞)
18		eqid 2209	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))) = (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅)))
19	8, 10, 12, 14, 17, 18	pw2f1odc 6964	. . . . 5 ⊢ (EXMID → (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))):𝒫 𝑥–1-1-onto→({∅, {∅}} ↑𝑚 𝑥))
20		f1oen2g 6876	. . . . 5 ⊢ ((𝒫 𝑥 ∈ V ∧ ({∅, {∅}} ↑𝑚 𝑥) ∈ V ∧ (𝑦 ∈ 𝒫 𝑥 ↦ (𝑧 ∈ 𝑥 ↦ if(𝑧 ∈ 𝑦, {∅}, ∅))):𝒫 𝑥–1-1-onto→({∅, {∅}} ↑𝑚 𝑥)) → 𝒫 𝑥 ≈ ({∅, {∅}} ↑𝑚 𝑥))
21	1, 7, 19, 20	mp3an12i 1356	. . . 4 ⊢ (EXMID → 𝒫 𝑥 ≈ ({∅, {∅}} ↑𝑚 𝑥))
22		df2o2 6547	. . . . 5 ⊢ 2o = {∅, {∅}}
23	22	oveq1i 5984	. . . 4 ⊢ (2o ↑𝑚 𝑥) = ({∅, {∅}} ↑𝑚 𝑥)
24	21, 23	breqtrrdi 4104	. . 3 ⊢ (EXMID → 𝒫 𝑥 ≈ (2o ↑𝑚 𝑥))
25	24	alrimiv 1900	. 2 ⊢ (EXMID → ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥))
26		1oex 6540	. . . . 5 ⊢ 1o ∈ V
27		pweq 3632	. . . . . 6 ⊢ (𝑥 = 1o → 𝒫 𝑥 = 𝒫 1o)
28		oveq2 5982	. . . . . 6 ⊢ (𝑥 = 1o → (2o ↑𝑚 𝑥) = (2o ↑𝑚 1o))
29	27, 28	breq12d 4075	. . . . 5 ⊢ (𝑥 = 1o → (𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) ↔ 𝒫 1o ≈ (2o ↑𝑚 1o)))
30	26, 29	spcv 2877	. . . 4 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → 𝒫 1o ≈ (2o ↑𝑚 1o))
31		df1o2 6545	. . . . . 6 ⊢ 1o = {∅}
32	31	oveq2i 5985	. . . . 5 ⊢ (2o ↑𝑚 1o) = (2o ↑𝑚 {∅})
33	22, 2	eqeltri 2282	. . . . . 6 ⊢ 2o ∈ V
34	33, 9	mapsnen 6934	. . . . 5 ⊢ (2o ↑𝑚 {∅}) ≈ 2o
35	32, 34	eqbrtri 4083	. . . 4 ⊢ (2o ↑𝑚 1o) ≈ 2o
36		entr 6906	. . . 4 ⊢ ((𝒫 1o ≈ (2o ↑𝑚 1o) ∧ (2o ↑𝑚 1o) ≈ 2o) → 𝒫 1o ≈ 2o)
37	30, 35, 36	sylancl 413	. . 3 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → 𝒫 1o ≈ 2o)
38		exmidpw 7038	. . 3 ⊢ (EXMID ↔ 𝒫 1o ≈ 2o)
39	37, 38	sylibr 134	. 2 ⊢ (∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥) → EXMID)
40	25, 39	impbii 126	1 ⊢ (EXMID ↔ ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥))

Syntax hints:   ↔ wb 105  DECID wdc 838  ∀wal 1373   = wceq 1375   ∈ wcel 2180  {cab 2195   ≠ wne 2380  ∀wral 2488  Vcvv 2779  ∅c0 3471  ifcif 3582  𝒫 cpw 3629  {csn 3646  {cpr 3647   class class class wbr 4062   ↦ cmpt 4124  EXMIDwem 4257  ⟶wf 5290  –1-1-onto→wf1o 5293  (class class class)co 5974  1_oc1o 6525  2_oc2o 6526   ↑_𝑚 cmap 6765   ≈ cen 6855

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 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606

This theorem depends on definitions:  df-bi 117  df-stab 835  df-dc 839  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-if 3583  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-tr 4162  df-exmid 4258  df-id 4361  df-iord 4434  df-on 4436  df-suc 4439  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-1o 6532  df-2o 6533  df-er 6650  df-map 6767  df-en 6858

This theorem is referenced by: (None)