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 limelon ⊢ A ∈ V ∧ Lim ⁡ A → A ∈ On
42 ffn ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → f Fn cf ⁡ ℵ ⁡ A
43 fnrnfv ⊢ f Fn cf ⁡ ℵ ⁡ A → ran ⁡ f = y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
44 43 unieqd ⊢ f Fn cf ⁡ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
45 42 44 syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
46 fvex ⊢ f ⁡ x ∈ V
47 46 dfiun2 ⊢ ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ⋃ y | ∃ x ∈ cf ⁡ ℵ ⁡ A y = f ⁡ x
48 45 47 eqtr4di ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ ran ⁡ f = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
49 48 ad2antrl ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ ran ⁡ f = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
50 fnfvelrn ⊢ f Fn cf ⁡ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A → f ⁡ w ∈ ran ⁡ f
51 42 50 sylan ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A → f ⁡ w ∈ ran ⁡ f
52 sseq2 ⊢ y = f ⁡ w → z ⊆ y ↔ z ⊆ f ⁡ w
53 52 rspcev ⊢ f ⁡ w ∈ ran ⁡ f ∧ z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
54 51 53 sylan ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ w ∈ cf ⁡ ℵ ⁡ A ∧ z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
55 54 rexlimdva2 ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∃ y ∈ ran ⁡ f z ⊆ y
56 55 ralimdv ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
57 56 imp ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
58 57 adantl ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
59 alephislim ⊢ A ∈ On ↔ Lim ⁡ ℵ ⁡ A
60 59 biimpi ⊢ A ∈ On → Lim ⁡ ℵ ⁡ A
61 frn ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ran ⁡ f ⊆ ℵ ⁡ A
62 61 adantr ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ran ⁡ f ⊆ ℵ ⁡ A
63 coflim ⊢ Lim ⁡ ℵ ⁡ A ∧ ran ⁡ f ⊆ ℵ ⁡ A → ⋃ ran ⁡ f = ℵ ⁡ A ↔ ∀ z ∈ ℵ ⁡ A ∃ y ∈ ran ⁡ f z ⊆ y
64 60 62 63 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
65 58 64 mpbird ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ ran ⁡ f = ℵ ⁡ A
66 49 65 eqtr3d ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ℵ ⁡ A
67 ffvelcdm ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ∈ ℵ ⁡ A
68 16 oneli ⊢ f ⁡ x ∈ ℵ ⁡ A → f ⁡ x ∈ On
69 harcard ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x
70 iscard ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x ↔ har ⁡ f ⁡ x ∈ On ∧ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
71 70 simprbi ⊢ card ⁡ har ⁡ f ⁡ x = har ⁡ f ⁡ x → ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
72 69 71 ax-mp ⊢ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x
73 domrefg ⊢ f ⁡ x ∈ V → f ⁡ x ≼ f ⁡ x
74 46 73 ax-mp ⊢ f ⁡ x ≼ f ⁡ x
75 elharval ⊢ f ⁡ x ∈ har ⁡ f ⁡ x ↔ f ⁡ x ∈ On ∧ f ⁡ x ≼ f ⁡ x
76 75 biimpri ⊢ f ⁡ x ∈ On ∧ f ⁡ x ≼ f ⁡ x → f ⁡ x ∈ har ⁡ f ⁡ x
77 74 76 mpan2 ⊢ f ⁡ x ∈ On → f ⁡ x ∈ har ⁡ f ⁡ x
78 breq1 ⊢ y = f ⁡ x → y ≺ har ⁡ f ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
79 78 rspccv ⊢ ∀ y ∈ har ⁡ f ⁡ x y ≺ har ⁡ f ⁡ x → f ⁡ x ∈ har ⁡ f ⁡ x → f ⁡ x ≺ har ⁡ f ⁡ x
80 72 77 79 mpsyl ⊢ f ⁡ x ∈ On → f ⁡ x ≺ har ⁡ f ⁡ x
81 67 68 80 3syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ har ⁡ f ⁡ x
82 harcl ⊢ har ⁡ f ⁡ x ∈ On
83 2fveq3 ⊢ y = x → har ⁡ f ⁡ y = har ⁡ f ⁡ x
84 83 1 fvmptg ⊢ x ∈ cf ⁡ ℵ ⁡ A ∧ har ⁡ f ⁡ x ∈ On → H ⁡ x = har ⁡ f ⁡ x
85 82 84 mpan2 ⊢ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x = har ⁡ f ⁡ x
86 85 breq2d ⊢ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
87 86 adantl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x ↔ f ⁡ x ≺ har ⁡ f ⁡ x
88 81 87 mpbird ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ≺ H ⁡ x
89 88 ralrimiva ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ H ⁡ x
90 fvex ⊢ cf ⁡ ℵ ⁡ A ∈ V
91 eqid ⊢ ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x = ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x
92 eqid ⊢ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x = ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
93 90 91 92 konigth ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ H ⁡ x → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
94 89 93 syl ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⋃ x ∈ cf ⁡ ℵ ⁡ A f ⁡ x ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
95 94 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
96 66 95 eqbrtrrd ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
97 41 96 sylan ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x
98 ovex ⊢ ℵ ⁡ A cf ⁡ ℵ ⁡ A ∈ V
99 67 ex ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → x ∈ cf ⁡ ℵ ⁡ A → f ⁡ x ∈ ℵ ⁡ A
100 alephlim ⊢ A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A = ⋃ y ∈ A ℵ ⁡ y
101 100 eleq2d ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ℵ ⁡ A ↔ f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y
102 eliun ⊢ f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y ↔ ∃ y ∈ A f ⁡ x ∈ ℵ ⁡ y
103 alephcard ⊢ card ⁡ ℵ ⁡ y = ℵ ⁡ y
104 103 eleq2i ⊢ f ⁡ x ∈ card ⁡ ℵ ⁡ y ↔ f ⁡ x ∈ ℵ ⁡ y
105 cardsdomelir ⊢ f ⁡ x ∈ card ⁡ ℵ ⁡ y → f ⁡ x ≺ ℵ ⁡ y
106 104 105 sylbir ⊢ f ⁡ x ∈ ℵ ⁡ y → f ⁡ x ≺ ℵ ⁡ y
107 elharval ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x ↔ ℵ ⁡ y ∈ On ∧ ℵ ⁡ y ≼ f ⁡ x
108 107 simprbi ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x → ℵ ⁡ y ≼ f ⁡ x
109 domnsym ⊢ ℵ ⁡ y ≼ f ⁡ x → ¬ f ⁡ x ≺ ℵ ⁡ y
110 108 109 syl ⊢ ℵ ⁡ y ∈ har ⁡ f ⁡ x → ¬ f ⁡ x ≺ ℵ ⁡ y
111 110 con2i ⊢ f ⁡ x ≺ ℵ ⁡ y → ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
112 alephon ⊢ ℵ ⁡ y ∈ On
113 ontri1 ⊢ har ⁡ f ⁡ x ∈ On ∧ ℵ ⁡ y ∈ On → har ⁡ f ⁡ x ⊆ ℵ ⁡ y ↔ ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
114 82 112 113 mp2an ⊢ har ⁡ f ⁡ x ⊆ ℵ ⁡ y ↔ ¬ ℵ ⁡ y ∈ har ⁡ f ⁡ x
115 111 114 sylibr ⊢ f ⁡ x ≺ ℵ ⁡ y → har ⁡ f ⁡ x ⊆ ℵ ⁡ y
116 106 115 syl ⊢ f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ⊆ ℵ ⁡ y
117 alephord2i ⊢ A ∈ On → y ∈ A → ℵ ⁡ y ∈ ℵ ⁡ A
118 117 imp ⊢ A ∈ On ∧ y ∈ A → ℵ ⁡ y ∈ ℵ ⁡ A
119 ontr2 ⊢ har ⁡ f ⁡ x ∈ On ∧ ℵ ⁡ A ∈ On → har ⁡ f ⁡ x ⊆ ℵ ⁡ y ∧ ℵ ⁡ y ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
120 82 16 119 mp2an ⊢ har ⁡ f ⁡ x ⊆ ℵ ⁡ y ∧ ℵ ⁡ y ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
121 116 118 120 syl2anr ⊢ A ∈ On ∧ y ∈ A ∧ f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
122 121 rexlimdva2 ⊢ A ∈ On → ∃ y ∈ A f ⁡ x ∈ ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
123 102 122 biimtrid ⊢ A ∈ On → f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
124 41 123 syl ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ⋃ y ∈ A ℵ ⁡ y → har ⁡ f ⁡ x ∈ ℵ ⁡ A
125 101 124 sylbid ⊢ A ∈ V ∧ Lim ⁡ A → f ⁡ x ∈ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
126 99 125 sylan9r ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → x ∈ cf ⁡ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
127 126 imp ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → har ⁡ f ⁡ x ∈ ℵ ⁡ A
128 83 cbvmptv ⊢ y ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ y = x ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ x
129 1 128 eqtri ⊢ H = x ∈ cf ⁡ ℵ ⁡ A ⟼ har ⁡ f ⁡ x
130 127 129 fmptd ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A
131 ffvelcdm ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x ∈ ℵ ⁡ A
132 onelss ⊢ ℵ ⁡ A ∈ On → H ⁡ x ∈ ℵ ⁡ A → H ⁡ x ⊆ ℵ ⁡ A
133 16 131 132 mpsyl ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ x ∈ cf ⁡ ℵ ⁡ A → H ⁡ x ⊆ ℵ ⁡ A
134 133 ralrimiva ⊢ H : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A
135 ss2ixp ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ⨉ x ∈ cf ⁡ ℵ ⁡ A ℵ ⁡ A
136 90 11 ixpconst ⊢ ⨉ x ∈ cf ⁡ ℵ ⁡ A ℵ ⁡ A = ℵ ⁡ A cf ⁡ ℵ ⁡ A
137 135 136 sseqtrdi ⊢ ∀ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A
138 130 134 137 3syl ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A
139 ssdomg ⊢ ℵ ⁡ A cf ⁡ ℵ ⁡ A ∈ V → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ⊆ ℵ ⁡ A cf ⁡ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A
140 98 138 139 mpsyl ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A → ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A
141 140 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
142 sdomdomtr ⊢ ℵ ⁡ A ≺ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ∧ ⨉ x ∈ cf ⁡ ℵ ⁡ A H ⁡ x ≼ ℵ ⁡ A cf ⁡ ℵ ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
143 97 141 142 syl2anc ⊢ A ∈ V ∧ Lim ⁡ A ∧ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
144 143 expcom ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
145 144 3adant2 ⊢ f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w → A ∈ V ∧ Lim ⁡ A → ℵ ⁡ A ≺ ℵ ⁡ A cf ⁡ ℵ ⁡ A
146 cfsmo ⊢ ℵ ⁡ A ∈ On → ∃ f f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w
147 16 146 ax-mp ⊢ ∃ f f : cf ⁡ ℵ ⁡ A ⟶ ℵ ⁡ A ∧ Smo ⁡ f ∧ ∀ z ∈ ℵ ⁡ A ∃ w ∈ cf ⁡ ℵ ⁡ A z ⊆ f ⁡ w
148 145 147 exlimiiv ⊢ 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