Metamath Proof Explorer

Theorem dfac12k

Description: Equivalence of dfac12 and dfac12a , without using Regularity. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion dfac12k ⊢∀x∈On𝒫x∈dom⁡card↔∀y∈On𝒫ℵ⁡y∈dom⁡card

Proof

Step Hyp Ref Expression
1 alephon ⊢ℵ⁡y∈On
2 pweq ⊢x=ℵ⁡y→𝒫x=𝒫ℵ⁡y
3 2 eleq1d ⊢x=ℵ⁡y→𝒫x∈dom⁡card↔𝒫ℵ⁡y∈dom⁡card
4 3 rspcv ⊢ℵ⁡y∈On→∀x∈On𝒫x∈dom⁡card→𝒫ℵ⁡y∈dom⁡card
5 1 4 ax-mp ⊢∀x∈On𝒫x∈dom⁡card→𝒫ℵ⁡y∈dom⁡card
6 5 ralrimivw ⊢∀x∈On𝒫x∈dom⁡card→∀y∈On𝒫ℵ⁡y∈dom⁡card
7 omelon ⊢ω∈On
8 cardon ⊢card⁡x∈On
9 ontri1 ⊢ω∈On∧card⁡x∈On→ω⊆card⁡x↔¬card⁡x∈ω
10 7 8 9 mp2an ⊢ω⊆card⁡x↔¬card⁡x∈ω
11 cardidm ⊢card⁡card⁡x=card⁡x
12 cardalephex ⊢ω⊆card⁡x→card⁡card⁡x=card⁡x↔∃y∈Oncard⁡x=ℵ⁡y
13 11 12 mpbii ⊢ω⊆card⁡x→∃y∈Oncard⁡x=ℵ⁡y
14 r19.29 ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card∧∃y∈Oncard⁡x=ℵ⁡y→∃y∈On𝒫ℵ⁡y∈dom⁡card∧card⁡x=ℵ⁡y
15 pweq ⊢card⁡x=ℵ⁡y→𝒫card⁡x=𝒫ℵ⁡y
16 15 eleq1d ⊢card⁡x=ℵ⁡y→𝒫card⁡x∈dom⁡card↔𝒫ℵ⁡y∈dom⁡card
17 16 biimparc ⊢𝒫ℵ⁡y∈dom⁡card∧card⁡x=ℵ⁡y→𝒫card⁡x∈dom⁡card
18 17 rexlimivw ⊢∃y∈On𝒫ℵ⁡y∈dom⁡card∧card⁡x=ℵ⁡y→𝒫card⁡x∈dom⁡card
19 14 18 syl ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card∧∃y∈Oncard⁡x=ℵ⁡y→𝒫card⁡x∈dom⁡card
20 19 ex ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→∃y∈Oncard⁡x=ℵ⁡y→𝒫card⁡x∈dom⁡card
21 13 20 syl5 ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→ω⊆card⁡x→𝒫card⁡x∈dom⁡card
22 10 21 biimtrrid ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→¬card⁡x∈ω→𝒫card⁡x∈dom⁡card
23 nnfi ⊢card⁡x∈ω→card⁡x∈Fin
24 pwfi ⊢card⁡x∈Fin↔𝒫card⁡x∈Fin
25 23 24 sylib ⊢card⁡x∈ω→𝒫card⁡x∈Fin
26 finnum ⊢𝒫card⁡x∈Fin→𝒫card⁡x∈dom⁡card
27 25 26 syl ⊢card⁡x∈ω→𝒫card⁡x∈dom⁡card
28 22 27 pm2.61d2 ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→𝒫card⁡x∈dom⁡card
29 oncardid ⊢x∈On→card⁡x≈x
30 pwen ⊢card⁡x≈x→𝒫card⁡x≈𝒫x
31 ennum ⊢𝒫card⁡x≈𝒫x→𝒫card⁡x∈dom⁡card↔𝒫x∈dom⁡card
32 29 30 31 3syl ⊢x∈On→𝒫card⁡x∈dom⁡card↔𝒫x∈dom⁡card
33 28 32 syl5ibcom ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→x∈On→𝒫x∈dom⁡card
34 33 ralrimiv ⊢∀y∈On𝒫ℵ⁡y∈dom⁡card→∀x∈On𝒫x∈dom⁡card
35 6 34 impbii ⊢∀x∈On𝒫x∈dom⁡card↔∀y∈On𝒫ℵ⁡y∈dom⁡card