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 e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` y ) ) )
Assertion pwcfsdom 
|- ( aleph ` A ) ~< ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )

Proof

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