# Metamath Proof Explorer

## Theorem cfpwsdom

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

Ref Expression
Hypothesis cfpwsdom.1 ${⊢}{B}\in \mathrm{V}$
Assertion cfpwsdom ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cfpwsdom.1 ${⊢}{B}\in \mathrm{V}$
2 ovex ${⊢}{{B}}^{\aleph \left({A}\right)}\in \mathrm{V}$
3 2 cardid ${⊢}\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\approx \left({{B}}^{\aleph \left({A}\right)}\right)$
4 3 ensymi ${⊢}\left({{B}}^{\aleph \left({A}\right)}\right)\approx \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)$
5 fvex ${⊢}\aleph \left({A}\right)\in \mathrm{V}$
6 5 canth2 ${⊢}\aleph \left({A}\right)\prec 𝒫\aleph \left({A}\right)$
7 5 pw2en ${⊢}𝒫\aleph \left({A}\right)\approx \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)$
8 sdomentr ${⊢}\left(\aleph \left({A}\right)\prec 𝒫\aleph \left({A}\right)\wedge 𝒫\aleph \left({A}\right)\approx \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)\right)\to \aleph \left({A}\right)\prec \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)$
9 6 7 8 mp2an ${⊢}\aleph \left({A}\right)\prec \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)$
10 mapdom1 ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)\preccurlyeq \left({{B}}^{\aleph \left({A}\right)}\right)$
11 sdomdomtr ${⊢}\left(\aleph \left({A}\right)\prec \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)\wedge \left({{2}_{𝑜}}^{\aleph \left({A}\right)}\right)\preccurlyeq \left({{B}}^{\aleph \left({A}\right)}\right)\right)\to \aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)$
12 9 10 11 sylancr ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)$
13 ficard ${⊢}{{B}}^{\aleph \left({A}\right)}\in \mathrm{V}\to \left({{B}}^{\aleph \left({A}\right)}\in \mathrm{Fin}↔\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\right)$
14 2 13 ax-mp ${⊢}{{B}}^{\aleph \left({A}\right)}\in \mathrm{Fin}↔\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }$
15 fict ${⊢}{{B}}^{\aleph \left({A}\right)}\in \mathrm{Fin}\to \left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \mathrm{\omega }$
16 14 15 sylbir ${⊢}\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\to \left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \mathrm{\omega }$
17 alephgeom ${⊢}{A}\in \mathrm{On}↔\mathrm{\omega }\subseteq \aleph \left({A}\right)$
18 alephon ${⊢}\aleph \left({A}\right)\in \mathrm{On}$
19 ssdomg ${⊢}\aleph \left({A}\right)\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq \aleph \left({A}\right)\to \mathrm{\omega }\preccurlyeq \aleph \left({A}\right)\right)$
20 18 19 ax-mp ${⊢}\mathrm{\omega }\subseteq \aleph \left({A}\right)\to \mathrm{\omega }\preccurlyeq \aleph \left({A}\right)$
21 17 20 sylbi ${⊢}{A}\in \mathrm{On}\to \mathrm{\omega }\preccurlyeq \aleph \left({A}\right)$
22 domtr ${⊢}\left(\left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\preccurlyeq \aleph \left({A}\right)\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \aleph \left({A}\right)$
23 16 21 22 syl2an ${⊢}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\wedge {A}\in \mathrm{On}\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \aleph \left({A}\right)$
24 domnsym ${⊢}\left({{B}}^{\aleph \left({A}\right)}\right)\preccurlyeq \aleph \left({A}\right)\to ¬\aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)$
25 23 24 syl ${⊢}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\wedge {A}\in \mathrm{On}\right)\to ¬\aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)$
26 25 expcom ${⊢}{A}\in \mathrm{On}\to \left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\to ¬\aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)\right)$
27 26 con2d ${⊢}{A}\in \mathrm{On}\to \left(\aleph \left({A}\right)\prec \left({{B}}^{\aleph \left({A}\right)}\right)\to ¬\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\right)$
28 cardidm ${⊢}\mathrm{card}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)$
29 iscard3 ${⊢}\mathrm{card}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)↔\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$
30 elun ${⊢}\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)↔\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\vee \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph \right)$
31 df-or ${⊢}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\vee \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph \right)↔\left(¬\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph \right)$
32 29 30 31 3bitri ${⊢}\mathrm{card}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)↔\left(¬\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph \right)$
33 28 32 mpbi ${⊢}¬\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{\omega }\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph$
34 12 27 33 syl56 ${⊢}{A}\in \mathrm{On}\to \left({2}_{𝑜}\preccurlyeq {B}\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph \right)$
35 alephfnon ${⊢}\aleph Fn\mathrm{On}$
36 fvelrnb ${⊢}\aleph Fn\mathrm{On}\to \left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph ↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
37 35 36 ax-mp ${⊢}\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\in \mathrm{ran}\aleph ↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)$
38 34 37 syl6ib ${⊢}{A}\in \mathrm{On}\to \left({2}_{𝑜}\preccurlyeq {B}\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
39 eqid ${⊢}\left({y}\in \mathrm{cf}\left(\aleph \left({x}\right)\right)⟼\mathrm{har}\left({z}\left({y}\right)\right)\right)=\left({y}\in \mathrm{cf}\left(\aleph \left({x}\right)\right)⟼\mathrm{har}\left({z}\left({y}\right)\right)\right)$
40 39 pwcfsdom ${⊢}\aleph \left({x}\right)\prec \left({\aleph \left({x}\right)}^{\mathrm{cf}\left(\aleph \left({x}\right)\right)}\right)$
41 id ${⊢}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to \aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)$
42 fveq2 ${⊢}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to \mathrm{cf}\left(\aleph \left({x}\right)\right)=\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
43 41 42 oveq12d ${⊢}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to {\aleph \left({x}\right)}^{\mathrm{cf}\left(\aleph \left({x}\right)\right)}={\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}$
44 41 43 breq12d ${⊢}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to \left(\aleph \left({x}\right)\prec \left({\aleph \left({x}\right)}^{\mathrm{cf}\left(\aleph \left({x}\right)\right)}\right)↔\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\right)$
45 40 44 mpbii ${⊢}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
46 45 rexlimivw ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\aleph \left({x}\right)=\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
47 38 46 syl6 ${⊢}{A}\in \mathrm{On}\to \left({2}_{𝑜}\preccurlyeq {B}\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\right)$
48 47 imp ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
49 ensdomtr ${⊢}\left(\left({{B}}^{\aleph \left({A}\right)}\right)\approx \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\wedge \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
50 4 48 49 sylancr ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
51 fvex ${⊢}\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\in \mathrm{V}$
52 51 enref ${⊢}\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\approx \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
53 mapen ${⊢}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\approx \left({{B}}^{\aleph \left({A}\right)}\right)\wedge \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\approx \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\to \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
54 3 52 53 mp2an ${⊢}\left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)$
55 mapxpen ${⊢}\left({B}\in \mathrm{V}\wedge \aleph \left({A}\right)\in \mathrm{On}\wedge \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\in \mathrm{V}\right)\to \left({\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
56 1 18 51 55 mp3an ${⊢}\left({\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
57 54 56 entri ${⊢}\left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
58 sdomentr ${⊢}\left(\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\wedge \left({\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)}^{\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)}\right)\approx \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
59 50 57 58 sylancl ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
60 5 xpdom2 ${⊢}\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\to \left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\preccurlyeq \left(\aleph \left({A}\right)×\aleph \left({A}\right)\right)$
61 17 biimpi ${⊢}{A}\in \mathrm{On}\to \mathrm{\omega }\subseteq \aleph \left({A}\right)$
62 infxpen ${⊢}\left(\aleph \left({A}\right)\in \mathrm{On}\wedge \mathrm{\omega }\subseteq \aleph \left({A}\right)\right)\to \left(\aleph \left({A}\right)×\aleph \left({A}\right)\right)\approx \aleph \left({A}\right)$
63 18 61 62 sylancr ${⊢}{A}\in \mathrm{On}\to \left(\aleph \left({A}\right)×\aleph \left({A}\right)\right)\approx \aleph \left({A}\right)$
64 domentr ${⊢}\left(\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\preccurlyeq \left(\aleph \left({A}\right)×\aleph \left({A}\right)\right)\wedge \left(\aleph \left({A}\right)×\aleph \left({A}\right)\right)\approx \aleph \left({A}\right)\right)\to \left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\preccurlyeq \aleph \left({A}\right)$
65 60 63 64 syl2an ${⊢}\left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\wedge {A}\in \mathrm{On}\right)\to \left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\preccurlyeq \aleph \left({A}\right)$
66 nsuceq0 ${⊢}\mathrm{suc}{1}_{𝑜}\ne \varnothing$
67 dom0 ${⊢}\mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing ↔\mathrm{suc}{1}_{𝑜}=\varnothing$
68 66 67 nemtbir ${⊢}¬\mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing$
69 df-2o ${⊢}{2}_{𝑜}=\mathrm{suc}{1}_{𝑜}$
70 69 breq1i ${⊢}{2}_{𝑜}\preccurlyeq {B}↔\mathrm{suc}{1}_{𝑜}\preccurlyeq {B}$
71 breq2 ${⊢}{B}=\varnothing \to \left(\mathrm{suc}{1}_{𝑜}\preccurlyeq {B}↔\mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$
72 70 71 syl5bb ${⊢}{B}=\varnothing \to \left({2}_{𝑜}\preccurlyeq {B}↔\mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$
73 72 biimpcd ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \left({B}=\varnothing \to \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$
74 73 adantld ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \left(\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\varnothing \wedge {B}=\varnothing \right)\to \mathrm{suc}{1}_{𝑜}\preccurlyeq \varnothing \right)$
75 68 74 mtoi ${⊢}{2}_{𝑜}\preccurlyeq {B}\to ¬\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\varnothing \wedge {B}=\varnothing \right)$
76 mapdom2 ${⊢}\left(\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)\preccurlyeq \aleph \left({A}\right)\wedge ¬\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\varnothing \wedge {B}=\varnothing \right)\right)\to \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\preccurlyeq \left({{B}}^{\aleph \left({A}\right)}\right)$
77 65 75 76 syl2an ${⊢}\left(\left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\wedge {A}\in \mathrm{On}\right)\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\preccurlyeq \left({{B}}^{\aleph \left({A}\right)}\right)$
78 domnsym ${⊢}\left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\preccurlyeq \left({{B}}^{\aleph \left({A}\right)}\right)\to ¬\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
79 77 78 syl ${⊢}\left(\left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\wedge {A}\in \mathrm{On}\right)\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to ¬\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)$
80 79 expl ${⊢}\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\to \left(\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to ¬\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\right)$
81 80 com12 ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)\to ¬\left({{B}}^{\aleph \left({A}\right)}\right)\prec \left({{B}}^{\left(\aleph \left({A}\right)×\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)}\right)\right)$
82 59 81 mt2d ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to ¬\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)$
83 domtri ${⊢}\left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\in \mathrm{V}\wedge \aleph \left({A}\right)\in \mathrm{V}\right)\to \left(\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)↔¬\aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)$
84 51 5 83 mp2an ${⊢}\mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)↔¬\aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
85 84 biimpri ${⊢}¬\aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\to \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\preccurlyeq \aleph \left({A}\right)$
86 82 85 nsyl2 ${⊢}\left({A}\in \mathrm{On}\wedge {2}_{𝑜}\preccurlyeq {B}\right)\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
87 86 ex ${⊢}{A}\in \mathrm{On}\to \left({2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)$
88 fndm ${⊢}\aleph Fn\mathrm{On}\to \mathrm{dom}\aleph =\mathrm{On}$
89 35 88 ax-mp ${⊢}\mathrm{dom}\aleph =\mathrm{On}$
90 89 eleq2i ${⊢}{A}\in \mathrm{dom}\aleph ↔{A}\in \mathrm{On}$
91 ndmfv ${⊢}¬{A}\in \mathrm{dom}\aleph \to \aleph \left({A}\right)=\varnothing$
92 90 91 sylnbir ${⊢}¬{A}\in \mathrm{On}\to \aleph \left({A}\right)=\varnothing$
93 1n0 ${⊢}{1}_{𝑜}\ne \varnothing$
94 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
95 94 0sdom ${⊢}\varnothing \prec {1}_{𝑜}↔{1}_{𝑜}\ne \varnothing$
96 93 95 mpbir ${⊢}\varnothing \prec {1}_{𝑜}$
97 id ${⊢}\aleph \left({A}\right)=\varnothing \to \aleph \left({A}\right)=\varnothing$
98 oveq2 ${⊢}\aleph \left({A}\right)=\varnothing \to {{B}}^{\aleph \left({A}\right)}={{B}}^{\varnothing }$
99 map0e ${⊢}{B}\in \mathrm{V}\to {{B}}^{\varnothing }={1}_{𝑜}$
100 1 99 ax-mp ${⊢}{{B}}^{\varnothing }={1}_{𝑜}$
101 98 100 syl6eq ${⊢}\aleph \left({A}\right)=\varnothing \to {{B}}^{\aleph \left({A}\right)}={1}_{𝑜}$
102 101 fveq2d ${⊢}\aleph \left({A}\right)=\varnothing \to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)=\mathrm{card}\left({1}_{𝑜}\right)$
103 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
104 cardnn ${⊢}{1}_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left({1}_{𝑜}\right)={1}_{𝑜}$
105 103 104 ax-mp ${⊢}\mathrm{card}\left({1}_{𝑜}\right)={1}_{𝑜}$
106 102 105 syl6eq ${⊢}\aleph \left({A}\right)=\varnothing \to \mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)={1}_{𝑜}$
107 106 fveq2d ${⊢}\aleph \left({A}\right)=\varnothing \to \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)=\mathrm{cf}\left({1}_{𝑜}\right)$
108 df-1o ${⊢}{1}_{𝑜}=\mathrm{suc}\varnothing$
109 108 fveq2i ${⊢}\mathrm{cf}\left({1}_{𝑜}\right)=\mathrm{cf}\left(\mathrm{suc}\varnothing \right)$
110 0elon ${⊢}\varnothing \in \mathrm{On}$
111 cfsuc ${⊢}\varnothing \in \mathrm{On}\to \mathrm{cf}\left(\mathrm{suc}\varnothing \right)={1}_{𝑜}$
112 110 111 ax-mp ${⊢}\mathrm{cf}\left(\mathrm{suc}\varnothing \right)={1}_{𝑜}$
113 109 112 eqtri ${⊢}\mathrm{cf}\left({1}_{𝑜}\right)={1}_{𝑜}$
114 107 113 syl6eq ${⊢}\aleph \left({A}\right)=\varnothing \to \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)={1}_{𝑜}$
115 97 114 breq12d ${⊢}\aleph \left({A}\right)=\varnothing \to \left(\aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)↔\varnothing \prec {1}_{𝑜}\right)$
116 96 115 mpbiri ${⊢}\aleph \left({A}\right)=\varnothing \to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$
117 116 a1d ${⊢}\aleph \left({A}\right)=\varnothing \to \left({2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)$
118 92 117 syl ${⊢}¬{A}\in \mathrm{On}\to \left({2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)\right)$
119 87 118 pm2.61i ${⊢}{2}_{𝑜}\preccurlyeq {B}\to \aleph \left({A}\right)\prec \mathrm{cf}\left(\mathrm{card}\left({{B}}^{\aleph \left({A}\right)}\right)\right)$