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 limelon 
 |-  ( ( A e. _V /\ Lim A ) -> A e. On )
42 ffn 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> f Fn ( cf ` ( aleph ` A ) ) )
43 fnrnfv 
 |-  ( f Fn ( cf ` ( aleph ` A ) ) -> ran f = { y | E. x e. ( cf ` ( aleph ` A ) ) y = ( f ` x ) } )
44 43 unieqd 
 |-  ( f Fn ( cf ` ( aleph ` A ) ) -> U. ran f = U. { y | E. x e. ( cf ` ( aleph ` A ) ) y = ( f ` x ) } )
45 42 44 syl 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> U. ran f = U. { y | E. x e. ( cf ` ( aleph ` A ) ) y = ( f ` x ) } )
46 fvex 
 |-  ( f ` x ) e. _V
47 46 dfiun2 
 |-  U_ x e. ( cf ` ( aleph ` A ) ) ( f ` x ) = U. { y | E. x e. ( cf ` ( aleph ` A ) ) y = ( f ` x ) }
48 45 47 eqtr4di 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> U. ran f = U_ x e. ( cf ` ( aleph ` A ) ) ( f ` x ) )
49 48 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 ) )
50 fnfvelrn 
 |-  ( ( f Fn ( cf ` ( aleph ` A ) ) /\ w e. ( cf ` ( aleph ` A ) ) ) -> ( f ` w ) e. ran f )
51 42 50 sylan 
 |-  ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ w e. ( cf ` ( aleph ` A ) ) ) -> ( f ` w ) e. ran f )
52 sseq2 
 |-  ( y = ( f ` w ) -> ( z C_ y <-> z C_ ( f ` w ) ) )
53 52 rspcev 
 |-  ( ( ( f ` w ) e. ran f /\ z C_ ( f ` w ) ) -> E. y e. ran f z C_ y )
54 51 53 sylan 
 |-  ( ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ w e. ( cf ` ( aleph ` A ) ) ) /\ z C_ ( f ` w ) ) -> E. y e. ran f z C_ y )
55 54 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 ) )
56 55 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 ) )
57 56 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 )
58 57 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 )
59 alephislim 
 |-  ( A e. On <-> Lim ( aleph ` A ) )
60 59 biimpi 
 |-  ( A e. On -> Lim ( aleph ` A ) )
61 frn 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> ran f C_ ( aleph ` A ) )
62 61 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 ) )
63 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 ) )
64 60 62 63 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 ) )
65 58 64 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 ) )
66 49 65 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 ) )
67 ffvelcdm 
 |-  ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( f ` x ) e. ( aleph ` A ) )
68 16 oneli 
 |-  ( ( f ` x ) e. ( aleph ` A ) -> ( f ` x ) e. On )
69 harcard 
 |-  ( card ` ( har ` ( f ` x ) ) ) = ( har ` ( f ` x ) )
70 iscard 
 |-  ( ( card ` ( har ` ( f ` x ) ) ) = ( har ` ( f ` x ) ) <-> ( ( har ` ( f ` x ) ) e. On /\ A. y e. ( har ` ( f ` x ) ) y ~< ( har ` ( f ` x ) ) ) )
71 70 simprbi 
 |-  ( ( card ` ( har ` ( f ` x ) ) ) = ( har ` ( f ` x ) ) -> A. y e. ( har ` ( f ` x ) ) y ~< ( har ` ( f ` x ) ) )
72 69 71 ax-mp 
 |-  A. y e. ( har ` ( f ` x ) ) y ~< ( har ` ( f ` x ) )
73 domrefg 
 |-  ( ( f ` x ) e. _V -> ( f ` x ) ~<_ ( f ` x ) )
74 46 73 ax-mp 
 |-  ( f ` x ) ~<_ ( f ` x )
75 elharval 
 |-  ( ( f ` x ) e. ( har ` ( f ` x ) ) <-> ( ( f ` x ) e. On /\ ( f ` x ) ~<_ ( f ` x ) ) )
76 75 biimpri 
 |-  ( ( ( f ` x ) e. On /\ ( f ` x ) ~<_ ( f ` x ) ) -> ( f ` x ) e. ( har ` ( f ` x ) ) )
77 74 76 mpan2 
 |-  ( ( f ` x ) e. On -> ( f ` x ) e. ( har ` ( f ` x ) ) )
78 breq1 
 |-  ( y = ( f ` x ) -> ( y ~< ( har ` ( f ` x ) ) <-> ( f ` x ) ~< ( har ` ( f ` x ) ) ) )
79 78 rspccv 
 |-  ( A. y e. ( har ` ( f ` x ) ) y ~< ( har ` ( f ` x ) ) -> ( ( f ` x ) e. ( har ` ( f ` x ) ) -> ( f ` x ) ~< ( har ` ( f ` x ) ) ) )
80 72 77 79 mpsyl 
 |-  ( ( f ` x ) e. On -> ( f ` x ) ~< ( har ` ( f ` x ) ) )
81 67 68 80 3syl 
 |-  ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( f ` x ) ~< ( har ` ( f ` x ) ) )
82 harcl 
 |-  ( har ` ( f ` x ) ) e. On
83 2fveq3 
 |-  ( y = x -> ( har ` ( f ` y ) ) = ( har ` ( f ` x ) ) )
84 83 1 fvmptg 
 |-  ( ( x e. ( cf ` ( aleph ` A ) ) /\ ( har ` ( f ` x ) ) e. On ) -> ( H ` x ) = ( har ` ( f ` x ) ) )
85 82 84 mpan2 
 |-  ( x e. ( cf ` ( aleph ` A ) ) -> ( H ` x ) = ( har ` ( f ` x ) ) )
86 85 breq2d 
 |-  ( x e. ( cf ` ( aleph ` A ) ) -> ( ( f ` x ) ~< ( H ` x ) <-> ( f ` x ) ~< ( har ` ( f ` x ) ) ) )
87 86 adantl 
 |-  ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( ( f ` x ) ~< ( H ` x ) <-> ( f ` x ) ~< ( har ` ( f ` x ) ) ) )
88 81 87 mpbird 
 |-  ( ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( f ` x ) ~< ( H ` x ) )
89 88 ralrimiva 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> A. x e. ( cf ` ( aleph ` A ) ) ( f ` x ) ~< ( H ` x ) )
90 fvex 
 |-  ( cf ` ( aleph ` A ) ) e. _V
91 eqid 
 |-  U_ x e. ( cf ` ( aleph ` A ) ) ( f ` x ) = U_ x e. ( cf ` ( aleph ` A ) ) ( f ` x )
92 eqid 
 |-  X_ x e. ( cf ` ( aleph ` A ) ) ( H ` x ) = X_ x e. ( cf ` ( aleph ` A ) ) ( H ` x )
93 90 91 92 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 ) )
94 89 93 syl 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> U_ x e. ( cf ` ( aleph ` A ) ) ( f ` x ) ~< X_ x e. ( cf ` ( aleph ` A ) ) ( H ` x ) )
95 94 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 ) )
96 66 95 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 ) )
97 41 96 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 ) )
98 ovex 
 |-  ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) ) e. _V
99 67 ex 
 |-  ( f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> ( x e. ( cf ` ( aleph ` A ) ) -> ( f ` x ) e. ( aleph ` A ) ) )
100 alephlim 
 |-  ( ( A e. _V /\ Lim A ) -> ( aleph ` A ) = U_ y e. A ( aleph ` y ) )
101 100 eleq2d 
 |-  ( ( A e. _V /\ Lim A ) -> ( ( f ` x ) e. ( aleph ` A ) <-> ( f ` x ) e. U_ y e. A ( aleph ` y ) ) )
102 eliun 
 |-  ( ( f ` x ) e. U_ y e. A ( aleph ` y ) <-> E. y e. A ( f ` x ) e. ( aleph ` y ) )
103 alephcard 
 |-  ( card ` ( aleph ` y ) ) = ( aleph ` y )
104 103 eleq2i 
 |-  ( ( f ` x ) e. ( card ` ( aleph ` y ) ) <-> ( f ` x ) e. ( aleph ` y ) )
105 cardsdomelir 
 |-  ( ( f ` x ) e. ( card ` ( aleph ` y ) ) -> ( f ` x ) ~< ( aleph ` y ) )
106 104 105 sylbir 
 |-  ( ( f ` x ) e. ( aleph ` y ) -> ( f ` x ) ~< ( aleph ` y ) )
107 elharval 
 |-  ( ( aleph ` y ) e. ( har ` ( f ` x ) ) <-> ( ( aleph ` y ) e. On /\ ( aleph ` y ) ~<_ ( f ` x ) ) )
108 107 simprbi 
 |-  ( ( aleph ` y ) e. ( har ` ( f ` x ) ) -> ( aleph ` y ) ~<_ ( f ` x ) )
109 domnsym 
 |-  ( ( aleph ` y ) ~<_ ( f ` x ) -> -. ( f ` x ) ~< ( aleph ` y ) )
110 108 109 syl 
 |-  ( ( aleph ` y ) e. ( har ` ( f ` x ) ) -> -. ( f ` x ) ~< ( aleph ` y ) )
111 110 con2i 
 |-  ( ( f ` x ) ~< ( aleph ` y ) -> -. ( aleph ` y ) e. ( har ` ( f ` x ) ) )
112 alephon 
 |-  ( aleph ` y ) e. On
113 ontri1 
 |-  ( ( ( har ` ( f ` x ) ) e. On /\ ( aleph ` y ) e. On ) -> ( ( har ` ( f ` x ) ) C_ ( aleph ` y ) <-> -. ( aleph ` y ) e. ( har ` ( f ` x ) ) ) )
114 82 112 113 mp2an 
 |-  ( ( har ` ( f ` x ) ) C_ ( aleph ` y ) <-> -. ( aleph ` y ) e. ( har ` ( f ` x ) ) )
115 111 114 sylibr 
 |-  ( ( f ` x ) ~< ( aleph ` y ) -> ( har ` ( f ` x ) ) C_ ( aleph ` y ) )
116 106 115 syl 
 |-  ( ( f ` x ) e. ( aleph ` y ) -> ( har ` ( f ` x ) ) C_ ( aleph ` y ) )
117 alephord2i 
 |-  ( A e. On -> ( y e. A -> ( aleph ` y ) e. ( aleph ` A ) ) )
118 117 imp 
 |-  ( ( A e. On /\ y e. A ) -> ( aleph ` y ) e. ( aleph ` A ) )
119 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 ) ) )
120 82 16 119 mp2an 
 |-  ( ( ( har ` ( f ` x ) ) C_ ( aleph ` y ) /\ ( aleph ` y ) e. ( aleph ` A ) ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) )
121 116 118 120 syl2anr 
 |-  ( ( ( A e. On /\ y e. A ) /\ ( f ` x ) e. ( aleph ` y ) ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) )
122 121 rexlimdva2 
 |-  ( A e. On -> ( E. y e. A ( f ` x ) e. ( aleph ` y ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) ) )
123 102 122 biimtrid 
 |-  ( A e. On -> ( ( f ` x ) e. U_ y e. A ( aleph ` y ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) ) )
124 41 123 syl 
 |-  ( ( A e. _V /\ Lim A ) -> ( ( f ` x ) e. U_ y e. A ( aleph ` y ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) ) )
125 101 124 sylbid 
 |-  ( ( A e. _V /\ Lim A ) -> ( ( f ` x ) e. ( aleph ` A ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) ) )
126 99 125 sylan9r 
 |-  ( ( ( A e. _V /\ Lim A ) /\ f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) ) -> ( x e. ( cf ` ( aleph ` A ) ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) ) )
127 126 imp 
 |-  ( ( ( ( A e. _V /\ Lim A ) /\ f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( har ` ( f ` x ) ) e. ( aleph ` A ) )
128 83 cbvmptv 
 |-  ( y e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` y ) ) ) = ( x e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` x ) ) )
129 1 128 eqtri 
 |-  H = ( x e. ( cf ` ( aleph ` A ) ) |-> ( har ` ( f ` x ) ) )
130 127 129 fmptd 
 |-  ( ( ( A e. _V /\ Lim A ) /\ f : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) ) -> H : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) )
131 ffvelcdm 
 |-  ( ( H : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( H ` x ) e. ( aleph ` A ) )
132 onelss 
 |-  ( ( aleph ` A ) e. On -> ( ( H ` x ) e. ( aleph ` A ) -> ( H ` x ) C_ ( aleph ` A ) ) )
133 16 131 132 mpsyl 
 |-  ( ( H : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) /\ x e. ( cf ` ( aleph ` A ) ) ) -> ( H ` x ) C_ ( aleph ` A ) )
134 133 ralrimiva 
 |-  ( H : ( cf ` ( aleph ` A ) ) --> ( aleph ` A ) -> A. x e. ( cf ` ( aleph ` A ) ) ( H ` x ) C_ ( aleph ` A ) )
135 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 ) )
136 90 11 ixpconst 
 |-  X_ x e. ( cf ` ( aleph ` A ) ) ( aleph ` A ) = ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )
137 135 136 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 ) ) ) )
138 130 134 137 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 ) ) ) )
139 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 ) ) ) ) )
140 98 138 139 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 ) ) ) )
141 140 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 ) ) ) )
142 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 ) ) ) )
143 97 141 142 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 ) ) ) )
144 143 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 ) ) ) ) )
145 144 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 ) ) ) ) )
146 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 ) ) )
147 16 146 ax-mp 
 |-  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 ) )
148 145 147 exlimiiv 
 |-  ( ( 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 ) ) )