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 e. _V
Assertion cfpwsdom 
|- ( 2o ~<_ B -> ( aleph ` A ) ~< ( cf ` ( card ` ( B ^m ( aleph ` A ) ) ) ) )

Proof

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