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 ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∀ 𝑦 ∈ On 𝒫 ( ℵ ‘ 𝑦 ) ∈ dom card )

Proof

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