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≺ℵ⁡Acf⁡ℵ⁡A

Proof

Step Hyp Ref Expression
1 pwcfsdom.1 ⊢H=y∈cf⁡ℵ⁡A⟼har⁡f⁡y
2 onzsl ⊢A∈On↔A=∅∨∃x∈OnA=suc⁡x∨A∈V∧Lim⁡A
3 2 biimpi ⊢A∈On→A=∅∨∃x∈OnA=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→ℵ⁡Acf⁡ℵ⁡A=ℵ⁡Aℵ⁡A
32 31 breq2d ⊢cf⁡ℵ⁡A=ℵ⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A↔ℵ⁡A≺ℵ⁡Aℵ⁡A
33 30 32 syl5ibrcom ⊢A∈On→cf⁡ℵ⁡A=ℵ⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
34 10 33 syl5 ⊢A∈On→A=∅→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡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∈OnA=suc⁡x→cf⁡ℵ⁡A=ℵ⁡A
40 39 33 syl5 ⊢A∈On→∃x∈OnA=suc⁡x→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
41 cfsmo ⊢ℵ⁡A∈On→∃ff:cf⁡ℵ⁡A⟶ℵ⁡A∧Smo⁡f∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w
42 limelon ⊢A∈V∧Lim⁡A→A∈On
43 ffn ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→fFncf⁡ℵ⁡A
44 fnrnfv ⊢fFncf⁡ℵ⁡A→ran⁡f=y|∃x∈cf⁡ℵ⁡Ay=f⁡x
45 44 unieqd ⊢fFncf⁡ℵ⁡A→⋃ran⁡f=⋃y|∃x∈cf⁡ℵ⁡Ay=f⁡x
46 43 45 syl ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→⋃ran⁡f=⋃y|∃x∈cf⁡ℵ⁡Ay=f⁡x
47 fvex ⊢f⁡x∈V
48 47 dfiun2 ⊢⋃x∈cf⁡ℵ⁡Af⁡x=⋃y|∃x∈cf⁡ℵ⁡Ay=f⁡x
49 46 48 eqtr4di ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→⋃ran⁡f=⋃x∈cf⁡ℵ⁡Af⁡x
50 49 ad2antrl ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⋃ran⁡f=⋃x∈cf⁡ℵ⁡Af⁡x
51 fnfvelrn ⊢fFncf⁡ℵ⁡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⁡fz⊆y
55 52 54 sylan ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A∧w∈cf⁡ℵ⁡A∧z⊆f⁡w→∃y∈ran⁡fz⊆y
56 55 rexlimdva2 ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→∃w∈cf⁡ℵ⁡Az⊆f⁡w→∃y∈ran⁡fz⊆y
57 56 ralimdv ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→∀z∈ℵ⁡A∃y∈ran⁡fz⊆y
58 57 imp ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→∀z∈ℵ⁡A∃y∈ran⁡fz⊆y
59 58 adantl ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→∀z∈ℵ⁡A∃y∈ran⁡fz⊆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⁡ℵ⁡Az⊆f⁡w→ran⁡f⊆ℵ⁡A
64 coflim ⊢Lim⁡ℵ⁡A∧ran⁡f⊆ℵ⁡A→⋃ran⁡f=ℵ⁡A↔∀z∈ℵ⁡A∃y∈ran⁡fz⊆y
65 61 63 64 syl2an ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⋃ran⁡f=ℵ⁡A↔∀z∈ℵ⁡A∃y∈ran⁡fz⊆y
66 59 65 mpbird ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⋃ran⁡f=ℵ⁡A
67 50 66 eqtr3d ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⋃x∈cf⁡ℵ⁡Af⁡x=ℵ⁡A
68 ffvelcdm ⊢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⁡xy≺har⁡f⁡x
72 71 simprbi ⊢card⁡har⁡f⁡x=har⁡f⁡x→∀y∈har⁡f⁡xy≺har⁡f⁡x
73 70 72 ax-mp ⊢∀y∈har⁡f⁡xy≺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⁡xy≺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⁡ℵ⁡Af⁡x≺H⁡x
91 fvex ⊢cf⁡ℵ⁡A∈V
92 eqid ⊢⋃x∈cf⁡ℵ⁡Af⁡x=⋃x∈cf⁡ℵ⁡Af⁡x
93 eqid ⊢⨉x∈cf⁡ℵ⁡AH⁡x=⨉x∈cf⁡ℵ⁡AH⁡x
94 91 92 93 konigth ⊢∀x∈cf⁡ℵ⁡Af⁡x≺H⁡x→⋃x∈cf⁡ℵ⁡Af⁡x≺⨉x∈cf⁡ℵ⁡AH⁡x
95 90 94 syl ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A→⋃x∈cf⁡ℵ⁡Af⁡x≺⨉x∈cf⁡ℵ⁡AH⁡x
96 95 ad2antrl ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⋃x∈cf⁡ℵ⁡Af⁡x≺⨉x∈cf⁡ℵ⁡AH⁡x
97 67 96 eqbrtrrd ⊢A∈On∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→ℵ⁡A≺⨉x∈cf⁡ℵ⁡AH⁡x
98 42 97 sylan ⊢A∈V∧Lim⁡A∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→ℵ⁡A≺⨉x∈cf⁡ℵ⁡AH⁡x
99 ovex ⊢ℵ⁡Acf⁡ℵ⁡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∈Af⁡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∈Af⁡x∈ℵ⁡y→har⁡f⁡x∈ℵ⁡A
124 103 123 biimtrid ⊢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 ffvelcdm ⊢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⁡ℵ⁡AH⁡x⊆ℵ⁡A
136 ss2ixp ⊢∀x∈cf⁡ℵ⁡AH⁡x⊆ℵ⁡A→⨉x∈cf⁡ℵ⁡AH⁡x⊆⨉x∈cf⁡ℵ⁡Aℵ⁡A
137 91 11 ixpconst ⊢⨉x∈cf⁡ℵ⁡Aℵ⁡A=ℵ⁡Acf⁡ℵ⁡A
138 136 137 sseqtrdi ⊢∀x∈cf⁡ℵ⁡AH⁡x⊆ℵ⁡A→⨉x∈cf⁡ℵ⁡AH⁡x⊆ℵ⁡Acf⁡ℵ⁡A
139 131 135 138 3syl ⊢A∈V∧Lim⁡A∧f:cf⁡ℵ⁡A⟶ℵ⁡A→⨉x∈cf⁡ℵ⁡AH⁡x⊆ℵ⁡Acf⁡ℵ⁡A
140 ssdomg ⊢ℵ⁡Acf⁡ℵ⁡A∈V→⨉x∈cf⁡ℵ⁡AH⁡x⊆ℵ⁡Acf⁡ℵ⁡A→⨉x∈cf⁡ℵ⁡AH⁡x≼ℵ⁡Acf⁡ℵ⁡A
141 99 139 140 mpsyl ⊢A∈V∧Lim⁡A∧f:cf⁡ℵ⁡A⟶ℵ⁡A→⨉x∈cf⁡ℵ⁡AH⁡x≼ℵ⁡Acf⁡ℵ⁡A
142 141 adantrr ⊢A∈V∧Lim⁡A∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→⨉x∈cf⁡ℵ⁡AH⁡x≼ℵ⁡Acf⁡ℵ⁡A
143 sdomdomtr ⊢ℵ⁡A≺⨉x∈cf⁡ℵ⁡AH⁡x∧⨉x∈cf⁡ℵ⁡AH⁡x≼ℵ⁡Acf⁡ℵ⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
144 98 142 143 syl2anc ⊢A∈V∧Lim⁡A∧f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
145 144 expcom ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
146 145 3adant2 ⊢f:cf⁡ℵ⁡A⟶ℵ⁡A∧Smo⁡f∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
147 146 exlimiv ⊢∃ff:cf⁡ℵ⁡A⟶ℵ⁡A∧Smo⁡f∧∀z∈ℵ⁡A∃w∈cf⁡ℵ⁡Az⊆f⁡w→A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
148 16 41 147 mp2b ⊢A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
149 148 a1i ⊢A∈On→A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
150 34 40 149 3jaod ⊢A∈On→A=∅∨∃x∈OnA=suc⁡x∨A∈V∧Lim⁡A→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
151 3 150 mpd ⊢A∈On→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
152 alephfnon ⊢ℵFnOn
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=∅→ℵ⁡Acf⁡ℵ⁡A=∅∅
165 0ex ⊢∅∈V
166 map0e ⊢∅∈V→∅∅=1𝑜
167 165 166 ax-mp ⊢∅∅=1𝑜
168 164 167 eqtrdi ⊢ℵ⁡A=∅→ℵ⁡Acf⁡ℵ⁡A=1𝑜
169 160 168 breq12d ⊢ℵ⁡A=∅→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A↔∅≺1𝑜
170 159 169 mpbiri ⊢ℵ⁡A=∅→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
171 155 170 syl ⊢¬A∈dom⁡ℵ→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
172 154 171 sylnbir ⊢¬A∈On→ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A
173 151 172 pm2.61i ⊢ℵ⁡A≺ℵ⁡Acf⁡ℵ⁡A