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 ∈ On card ⁡ x = ℵ ⁡ y
13 11 12 mpbii ⊢ ω ⊆ card ⁡ x → ∃ y ∈ On card ⁡ x = ℵ ⁡ y
14 r19.29 ⊢ ∀ y ∈ On 𝒫 ℵ ⁡ y ∈ dom ⁡ card ∧ ∃ y ∈ On card ⁡ 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 ∈ On card ⁡ x = ℵ ⁡ y → 𝒫 card ⁡ x ∈ dom ⁡ card
20 19 ex ⊢ ∀ y ∈ On 𝒫 ℵ ⁡ y ∈ dom ⁡ card → ∃ y ∈ On card ⁡ 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