Metamath Proof Explorer

Theorem pwcfsdom

Description: A corollary of Konig's Theorem konigth . Theorem 11.28 of TakeutiZaring p. 108. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Hypothesis pwcfsdom.1 ⊢ H = y ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ y
Assertion pwcfsdom ⊢ ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A

Proof

Step Hyp Ref Expression
1 pwcfsdom.1 ⊢ H = y ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ y
2 onzsl ⊢ A ∈ On ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
3 2 biimpi ⊢ A ∈ On → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
4 cfom ⊢ cf ⁡ ω = ω
5 aleph0 ⊢ ℵ ⁡ ∅ = ω
6 5 fveq2i ⊢ cf ⁡ ℵ ⁡ ∅ = cf ⁡ ω
7 4 6 5 3eqtr4i ⊢ cf ⁡ ℵ ⁡ ∅ = ℵ ⁡ ∅
8 2fveq3 ⊢ A = ∅ → cf ⁡ ℵ ⁡ A = cf ⁡ ℵ ⁡ ∅
9 fveq2 ⊢ A = ∅ → ℵ ⁡ A = ℵ ⁡ ∅
10 7 8 9 3eqtr4a ⊢ A = ∅ → cf ⁡ ℵ ⁡ A = ℵ ⁡ A
11 fvex ⊢ ℵ ⁡ A ∈ V
12 11 canth2 ⊢ ℵ ⁡ A ≺ 𝒫 ℵ ⁡ A
13 11 pw2en ⊢ 𝒫 ℵ ⁡ A ≈ 2 𝑜 ℵ ⁡ A
14 sdomentr ⊢ ℵ ⁡ A ≺ 𝒫 ℵ ⁡ A ∧ 𝒫 ℵ ⁡ A ≈ 2 𝑜 ℵ ⁡ A → ℵ ⁡ A ≺ 2 𝑜 ℵ ⁡ A
15 12 13 14 mp2an ⊢ ℵ ⁡ A ≺ 2 𝑜 ℵ ⁡ A
16 alephon ⊢ ℵ ⁡ A ∈ On
17 alephgeom ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A
18 omelon ⊢ ω ∈ On
19 2onn ⊢ 2 𝑜 ∈ ω
20 onelss ⊢ ω ∈ On → 2 𝑜 ∈ ω → 2 𝑜 ⊆ ω
21 18 19 20 mp2 ⊢ 2 𝑜 ⊆ ω
22 sstr ⊢ 2 𝑜 ⊆ ω ∧ ω ⊆ ℵ ⁡ A → 2 𝑜 ⊆ ℵ ⁡ A
23 21 22 mpan ⊢ ω ⊆ ℵ ⁡ A → 2 𝑜 ⊆ ℵ ⁡ A
24 17 23 sylbi ⊢ A ∈ On → 2 𝑜 ⊆ ℵ ⁡ A
25 ssdomg ⊢ ℵ ⁡ A ∈ On → 2 𝑜 ⊆ ℵ ⁡ A → 2 𝑜 ≼ ℵ ⁡ A
26 16 24 25 mpsyl ⊢ A ∈ On → 2 𝑜 ≼ ℵ ⁡ A
27 mapdom1 ⊢ 2 𝑜 ≼ ℵ ⁡ A → 2 𝑜 ℵ ⁡ A ≼ ℵ ⁡ A ℵ ⁡ A
28 26 27 syl ⊢ A ∈ On → 2 𝑜 ℵ ⁡ A ≼ ℵ ⁡ A ℵ ⁡ A
29 sdomdomtr ⊢ ℵ ⁡ A ≺ 2 𝑜 ℵ ⁡ A ∧ 2 𝑜 ℵ ⁡ A ≼ ℵ ⁡ A ℵ ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A ℵ ⁡ A
30 15 28 29 sylancr ⊢ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ A ℵ ⁡ A
31 oveq2 ⊢ cf ⁡ ℵ ⁡ A = ℵ ⁡ A → ℵ ⁡ A cf ⁡ ℵ ⁡ A = ℵ ⁡ A ℵ ⁡ A
32 31 breq2d ⊢ cf ⁡ ℵ ⁡ A = ℵ ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A ↔ ℵ ⁡ A ≺ ℵ ⁡ A ℵ ⁡ A
33 30 32 syl5ibrcom ⊢ A ∈ On → cf ⁡ ℵ ⁡ A = ℵ ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
34 10 33 syl5 ⊢ A ∈ On → A = ∅ → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
35 alephreg ⊢ cf ⁡ ℵ ⁡ suc ⁡ x = ℵ ⁡ suc ⁡ x
36 2fveq3 ⊢ A = suc ⁡ x → cf ⁡ ℵ ⁡ A = cf ⁡ ℵ ⁡ suc ⁡ x
37 fveq2 ⊢ A = suc ⁡ x → ℵ ⁡ A = ℵ ⁡ suc ⁡ x
38 35 36 37 3eqtr4a ⊢ A = suc ⁡ x → cf ⁡ ℵ ⁡ A = ℵ ⁡ A
39 38 rexlimivw ⊢ ∃ x ∈ On A = suc ⁡ x → cf ⁡ ℵ ⁡ A = ℵ ⁡ A
40 39 33 syl5 ⊢ A ∈ On → ∃ x ∈ On A = suc ⁡ x → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
41 cfsmo ⊢ ℵ ⁡ A ∈ On → ∃ f f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w
42 limelon ⊢ A ∈ V ∧ Lim ⁡ A → A ∈ On
43 ffn ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → f Fn cf ⁡ ℵ ⁡ A
44 fnrnfv ⊢ f Fn cf ⁡ ℵ ⁡ A → ran ⁡ f = y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
45 44 unieqd ⊢ f Fn cf ⁡ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
46 43 45 syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
47 fvex ⊢ f ⁡ x ∈ V
48 47 dfiun2 ⊢ ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
49 46 48 eqtr4di ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
50 49 ad2antrl ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ ran ⁡ f = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
51 fnfvelrn ⊢ f Fn cf ⁡ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A → f ⁡ w ∈ ran ⁡ f
52 43 51 sylan ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A → f ⁡ w ∈ ran ⁡ f
53 sseq2 ⊢ y = f ⁡ w → z ⊆ y ↔ z ⊆ f ⁡ w
54 53 rspcev ⊢ f ⁡ w ∈ ran ⁡ f ∧ z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
55 52 54 sylan ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A ∧ z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
56 55 rexlimdva2 ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
57 56 ralimdv ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
58 57 imp ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
59 58 adantl ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
60 alephislim ⊢ A ∈ On ↔ Lim ⁡ ℵ ⁡ A
61 60 biimpi ⊢ A ∈ On → Lim ⁡ ℵ ⁡ A
62 frn ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ran ⁡ f ⊆ ℵ ⁡ A
63 62 adantr ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ran ⁡ f ⊆ ℵ ⁡ A
64 coflim ⊢ Lim ⁡ ℵ ⁡ A ∧ ran ⁡ f ⊆ ℵ ⁡ A → ⋃ ran ⁡ f = ℵ ⁡ A ↔ ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
65 61 63 64 syl2an ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ ran ⁡ f = ℵ ⁡ A ↔ ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
66 59 65 mpbird ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ ran ⁡ f = ℵ ⁡ A
67 50 66 eqtr3d ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ℵ ⁡ A
68 ffvelrn ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ∈ ℵ ⁡ A
69 16 oneli ⊢ f ⁡ x ∈ ℵ ⁡ A → f ⁡ x ∈ On
70 harcard ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x
71 iscard ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x ↔ har ⁡ f ⁡ x ∈ On ∧ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
72 71 simprbi ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x → ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
73 70 72 ax-mp ⊢ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
74 domrefg ⊢ f ⁡ x ∈ V → f ⁡ x ≼ f ⁡ x
75 47 74 ax-mp ⊢ f ⁡ x ≼ f ⁡ x
76 elharval ⊢ f ⁡ x ∈ har ⁡ f ⁡ x ↔ f ⁡ x ∈ On ∧ f ⁡ x ≼ f ⁡ x
77 76 biimpri ⊢ f ⁡ x ∈ On ∧ f ⁡ x ≼ f ⁡ x → f ⁡ x ∈ har ⁡ f ⁡ x
78 75 77 mpan2 ⊢ f ⁡ x ∈ On → f ⁡ x ∈ har ⁡ f ⁡ x
79 breq1 ⊢ y = f ⁡ x → y ≺ har ⁡ f ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
80 79 rspccv ⊢ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x → f ⁡ x ∈ har ⁡ f ⁡ x → f ⁡ x ≺ har ⁡ f ⁡ x
81 73 78 80 mpsyl ⊢ f ⁡ x ∈ On → f ⁡ x ≺ har ⁡ f ⁡ x
82 68 69 81 3syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ har ⁡ f ⁡ x
83 harcl ⊢ har ⁡ f ⁡ x ∈ On
84 2fveq3 ⊢ y = x → har ⁡ f ⁡ y = har ⁡ f ⁡ x
85 84 1 fvmptg ⊢ x ∈ cf ⁡ ℵ ⁡ A ∧ har ⁡ f ⁡ x ∈ On → H ⁡ x = har ⁡ f ⁡ x
86 83 85 mpan2 ⊢ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x = har ⁡ f ⁡ x
87 86 breq2d ⊢ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
88 87 adantl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
89 82 88 mpbird ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x
90 89 ralrimiva ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ H ⁡ x
91 fvex ⊢ cf ⁡ ℵ ⁡ A ∈ V
92 eqid ⊢ ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
93 eqid ⊢ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x = ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
94 91 92 93 konigth ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ H ⁡ x → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
95 90 94 syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
96 95 ad2antrl ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
97 67 96 eqbrtrrd ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
98 42 97 sylan ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
99 ovex ⊢ ℵ ⁡ A cf ⁡ ℵ ⁡ A ∈ V
100 68 ex ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ∈ ℵ ⁡ A
101 alephlim ⊢ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A = ⋃ y ∈ A ℵ ⁡ y
102 101 eleq2d ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ℵ ⁡ A ↔ f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y
103 eliun ⊢ f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y ↔ ∃ y ∈ A f ⁡ x ∈ ℵ ⁡ y
104 alephcard ⊢ card ⁡ ℵ ⁡ y = ℵ ⁡ y
105 104 eleq2i ⊢ f ⁡ x ∈ card ⁡ ℵ ⁡ y ↔ f ⁡ x ∈ ℵ ⁡ y
106 cardsdomelir ⊢ f ⁡ x ∈ card ⁡ ℵ ⁡ y → f ⁡ x ≺ ℵ ⁡ y
107 105 106 sylbir ⊢ f ⁡ x ∈ ℵ ⁡ y → f ⁡ x ≺ ℵ ⁡ y
108 elharval ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x ↔ ℵ ⁡ y ∈ On ∧ ℵ ⁡ y ≼ f ⁡ x
109 108 simprbi ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x → ℵ ⁡ y ≼ f ⁡ x
110 domnsym ⊢ ℵ ⁡ y ≼ f ⁡ x → ¬ f ⁡ x ≺ ℵ ⁡ y
111 109 110 syl ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x → ¬ f ⁡ x ≺ ℵ ⁡ y
112 111 con2i ⊢ f ⁡ x ≺ ℵ ⁡ y → ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
113 alephon ⊢ ℵ ⁡ y ∈ On
114 ontri1 ⊢ har ⁡ f ⁡ x ∈ On ∧ ℵ ⁡ y ∈ On → har ⁡ f ⁡ x ⊆ ℵ ⁡ y ↔ ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
115 83 113 114 mp2an ⊢ har ⁡ f ⁡ x ⊆ ℵ ⁡ y ↔ ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
116 112 115 sylibr ⊢ f ⁡ x ≺ ℵ ⁡ y → har ⁡ f ⁡ x ⊆ ℵ ⁡ y
117 107 116 syl ⊢ f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ⊆ ℵ ⁡ y
118 alephord2i ⊢ A ∈ On → y ∈ A → ℵ ⁡ y ∈ ℵ ⁡ A
119 118 imp ⊢ A ∈ On ∧ y ∈ A → ℵ ⁡ y ∈ ℵ ⁡ A
120 ontr2 ⊢ har ⁡ f ⁡ x ∈ On ∧ ℵ ⁡ A ∈ On → har ⁡ f ⁡ x ⊆ ℵ ⁡ y ∧ ℵ ⁡ y ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
121 83 16 120 mp2an ⊢ har ⁡ f ⁡ x ⊆ ℵ ⁡ y ∧ ℵ ⁡ y ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
122 117 119 121 syl2anr ⊢ A ∈ On ∧ y ∈ A ∧ f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
123 122 rexlimdva2 ⊢ A ∈ On → ∃ y ∈ A f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
124 103 123 syl5bi ⊢ A ∈ On → f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
125 42 124 syl ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
126 102 125 sylbid ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
127 100 126 sylan9r ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → x ∈ cf ⁡ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
128 127 imp ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
129 84 cbvmptv ⊢ y ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ y = x ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ x
130 1 129 eqtri ⊢ H = x ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ x
131 128 130 fmptd ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A
132 ffvelrn ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x ∈ ℵ ⁡ A
133 onelss ⊢ ℵ ⁡ A ∈ On → H ⁡ x ∈ ℵ ⁡ A → H ⁡ x ⊆ ℵ ⁡ A
134 16 132 133 mpsyl ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x ⊆ ℵ ⁡ A
135 134 ralrimiva ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A
136 ss2ixp ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ⨉ x ∈ cf ⁡ ℵ ⁡ A ℵ ⁡ A
137 91 11 ixpconst ⊢ ⨉ x ∈ cf ⁡ ℵ ⁡ A ℵ ⁡ A = ℵ ⁡ A cf ⁡ ℵ ⁡ A
138 136 137 sseqtrdi ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A
139 131 135 138 3syl ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A
140 ssdomg ⊢ ℵ ⁡ A cf ⁡ ℵ ⁡ A ∈ V → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A
141 99 139 140 mpsyl ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A
142 141 adantrr ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A
143 sdomdomtr ⊢ ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ∧ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
144 98 142 143 syl2anc ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
145 144 expcom ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
146 145 3adant2 ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
147 146 exlimiv ⊢ ∃ f f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
148 16 41 147 mp2b ⊢ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
149 148 a1i ⊢ A ∈ On → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
150 34 40 149 3jaod ⊢ A ∈ On → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
151 3 150 mpd ⊢ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
152 alephfnon ⊢ ℵ Fn On
153 152 fndmi ⊢ dom ⁡ ℵ = On
154 153 eleq2i ⊢ A ∈ dom ⁡ ℵ ↔ A ∈ On
155 ndmfv ⊢ ¬ A ∈ dom ⁡ ℵ → ℵ ⁡ A = ∅
156 1n0 ⊢ 1 𝑜 ≠ ∅
157 1oex ⊢ 1 𝑜 ∈ V
158 157 0sdom ⊢ ∅ ≺ 1 𝑜 ↔ 1 𝑜 ≠ ∅
159 156 158 mpbir ⊢ ∅ ≺ 1 𝑜
160 id ⊢ ℵ ⁡ A = ∅ → ℵ ⁡ A = ∅
161 fveq2 ⊢ ℵ ⁡ A = ∅ → cf ⁡ ℵ ⁡ A = cf ⁡ ∅
162 cf0 ⊢ cf ⁡ ∅ = ∅
163 161 162 eqtrdi ⊢ ℵ ⁡ A = ∅ → cf ⁡ ℵ ⁡ A = ∅
164 160 163 oveq12d ⊢ ℵ ⁡ A = ∅ → ℵ ⁡ A cf ⁡ ℵ ⁡ A = ∅ ∅
165 0ex ⊢ ∅ ∈ V
166 map0e ⊢ ∅ ∈ V → ∅ ∅ = 1 𝑜
167 165 166 ax-mp ⊢ ∅ ∅ = 1 𝑜
168 164 167 eqtrdi ⊢ ℵ ⁡ A = ∅ → ℵ ⁡ A cf ⁡ ℵ ⁡ A = 1 𝑜
169 160 168 breq12d ⊢ ℵ ⁡ A = ∅ → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A ↔ ∅ ≺ 1 𝑜
170 159 169 mpbiri ⊢ ℵ ⁡ A = ∅ → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
171 155 170 syl ⊢ ¬ A ∈ dom ⁡ ℵ → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
172 154 171 sylnbir ⊢ ¬ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
173 151 172 pm2.61i ⊢ ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A