Metamath Proof Explorer

Theorem cofsmo

Description: Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of TakeutiZaring p. 101. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Hypotheses cofsmo.1 
|- C = { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) }
cofsmo.2 
|- K = |^| { x e. B | z C_ ( f ` x ) }
cofsmo.3 
|- O = OrdIso ( _E , C )
Assertion cofsmo 
|- ( ( Ord A /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )

Proof

Step Hyp Ref Expression
1 cofsmo.1 
 |-  C = { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) }
2 cofsmo.2 
 |-  K = |^| { x e. B | z C_ ( f ` x ) }
3 cofsmo.3 
 |-  O = OrdIso ( _E , C )
4 1 ssrab3 
 |-  C C_ B
5 ssexg 
 |-  ( ( C C_ B /\ B e. On ) -> C e. _V )
6 4 5 mpan 
 |-  ( B e. On -> C e. _V )
7 onss 
 |-  ( B e. On -> B C_ On )
8 4 7 sstrid 
 |-  ( B e. On -> C C_ On )
9 epweon 
 |-  _E We On
10 wess 
 |-  ( C C_ On -> ( _E We On -> _E We C ) )
11 8 9 10 mpisyl 
 |-  ( B e. On -> _E We C )
12 3 oiiso 
 |-  ( ( C e. _V /\ _E We C ) -> O Isom _E , _E ( dom O , C ) )
13 6 11 12 syl2anc 
 |-  ( B e. On -> O Isom _E , _E ( dom O , C ) )
14 13 ad2antlr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O Isom _E , _E ( dom O , C ) )
15 isof1o 
 |-  ( O Isom _E , _E ( dom O , C ) -> O : dom O -1-1-onto-> C )
16 f1ofo 
 |-  ( O : dom O -1-1-onto-> C -> O : dom O -onto-> C )
17 14 15 16 3syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O -onto-> C )
18 fof 
 |-  ( O : dom O -onto-> C -> O : dom O --> C )
19 fss 
 |-  ( ( O : dom O --> C /\ C C_ B ) -> O : dom O --> B )
20 18 4 19 sylancl 
 |-  ( O : dom O -onto-> C -> O : dom O --> B )
21 17 20 syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O --> B )
22 3 oion 
 |-  ( C e. _V -> dom O e. On )
23 6 22 syl 
 |-  ( B e. On -> dom O e. On )
24 23 ad2antlr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O e. On )
25 simplr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> B e. On )
26 eloni 
 |-  ( dom O e. On -> Ord dom O )
27 smoiso2 
 |-  ( ( Ord dom O /\ C C_ On ) -> ( ( O : dom O -onto-> C /\ Smo O ) <-> O Isom _E , _E ( dom O , C ) ) )
28 26 8 27 syl2an 
 |-  ( ( dom O e. On /\ B e. On ) -> ( ( O : dom O -onto-> C /\ Smo O ) <-> O Isom _E , _E ( dom O , C ) ) )
29 28 biimpar 
 |-  ( ( ( dom O e. On /\ B e. On ) /\ O Isom _E , _E ( dom O , C ) ) -> ( O : dom O -onto-> C /\ Smo O ) )
30 29 simprd 
 |-  ( ( ( dom O e. On /\ B e. On ) /\ O Isom _E , _E ( dom O , C ) ) -> Smo O )
31 24 25 14 30 syl21anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Smo O )
32 eloni 
 |-  ( B e. On -> Ord B )
33 32 ad2antlr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Ord B )
34 smocdmdom 
 |-  ( ( O : dom O --> B /\ Smo O /\ Ord B ) -> dom O C_ B )
35 21 31 33 34 syl3anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O C_ B )
36 onsssuc 
 |-  ( ( dom O e. On /\ B e. On ) -> ( dom O C_ B <-> dom O e. suc B ) )
37 24 25 36 syl2anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( dom O C_ B <-> dom O e. suc B ) )
38 35 37 mpbid 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> dom O e. suc B )
39 38 adantrr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> dom O e. suc B )
40 vex 
 |-  f e. _V
41 3 oiexg 
 |-  ( C e. _V -> O e. _V )
42 6 41 syl 
 |-  ( B e. On -> O e. _V )
43 42 ad2antlr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> O e. _V )
44 coexg 
 |-  ( ( f e. _V /\ O e. _V ) -> ( f o. O ) e. _V )
45 40 43 44 sylancr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( f o. O ) e. _V )
46 simprl 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> f : B --> A )
47 21 adantrr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> O : dom O --> B )
48 46 47 fcod 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( f o. O ) : dom O --> A )
49 simpr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> f : B --> A )
50 49 21 fcod 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( f o. O ) : dom O --> A )
51 ordsson 
 |-  ( Ord A -> A C_ On )
52 51 ad2antrr 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> A C_ On )
53 24 26 syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Ord dom O )
54 17 18 syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O : dom O --> C )
55 simpl 
 |-  ( ( s e. dom O /\ t e. s ) -> s e. dom O )
56 ffvelcdm 
 |-  ( ( O : dom O --> C /\ s e. dom O ) -> ( O ` s ) e. C )
57 54 55 56 syl2an 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` s ) e. C )
58 ffn 
 |-  ( O : dom O --> C -> O Fn dom O )
59 17 18 58 3syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> O Fn dom O )
60 59 31 jca 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( O Fn dom O /\ Smo O ) )
61 smoel2 
 |-  ( ( ( O Fn dom O /\ Smo O ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` t ) e. ( O ` s ) )
62 60 61 sylan 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( O ` t ) e. ( O ` s ) )
63 fveq2 
 |-  ( z = ( O ` s ) -> ( f ` z ) = ( f ` ( O ` s ) ) )
64 63 eleq2d 
 |-  ( z = ( O ` s ) -> ( ( f ` x ) e. ( f ` z ) <-> ( f ` x ) e. ( f ` ( O ` s ) ) ) )
65 64 raleqbi1dv 
 |-  ( z = ( O ` s ) -> ( A. x e. z ( f ` x ) e. ( f ` z ) <-> A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) ) )
66 fveq2 
 |-  ( w = x -> ( f ` w ) = ( f ` x ) )
67 66 eleq1d 
 |-  ( w = x -> ( ( f ` w ) e. ( f ` y ) <-> ( f ` x ) e. ( f ` y ) ) )
68 67 cbvralvw 
 |-  ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. x e. y ( f ` x ) e. ( f ` y ) )
69 fveq2 
 |-  ( y = z -> ( f ` y ) = ( f ` z ) )
70 69 eleq2d 
 |-  ( y = z -> ( ( f ` x ) e. ( f ` y ) <-> ( f ` x ) e. ( f ` z ) ) )
71 70 raleqbi1dv 
 |-  ( y = z -> ( A. x e. y ( f ` x ) e. ( f ` y ) <-> A. x e. z ( f ` x ) e. ( f ` z ) ) )
72 68 71 bitrid 
 |-  ( y = z -> ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. x e. z ( f ` x ) e. ( f ` z ) ) )
73 72 cbvrabv 
 |-  { y e. B | A. w e. y ( f ` w ) e. ( f ` y ) } = { z e. B | A. x e. z ( f ` x ) e. ( f ` z ) }
74 1 73 eqtri 
 |-  C = { z e. B | A. x e. z ( f ` x ) e. ( f ` z ) }
75 65 74 elrab2 
 |-  ( ( O ` s ) e. C <-> ( ( O ` s ) e. B /\ A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) ) )
76 75 simprbi 
 |-  ( ( O ` s ) e. C -> A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) )
77 fveq2 
 |-  ( x = ( O ` t ) -> ( f ` x ) = ( f ` ( O ` t ) ) )
78 77 eleq1d 
 |-  ( x = ( O ` t ) -> ( ( f ` x ) e. ( f ` ( O ` s ) ) <-> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
79 78 rspccv 
 |-  ( A. x e. ( O ` s ) ( f ` x ) e. ( f ` ( O ` s ) ) -> ( ( O ` t ) e. ( O ` s ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
80 76 79 syl 
 |-  ( ( O ` s ) e. C -> ( ( O ` t ) e. ( O ` s ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) ) )
81 57 62 80 sylc 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( f ` ( O ` t ) ) e. ( f ` ( O ` s ) ) )
82 ordtr1 
 |-  ( Ord dom O -> ( ( t e. s /\ s e. dom O ) -> t e. dom O ) )
83 82 ancomsd 
 |-  ( Ord dom O -> ( ( s e. dom O /\ t e. s ) -> t e. dom O ) )
84 24 26 83 3syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( ( s e. dom O /\ t e. s ) -> t e. dom O ) )
85 84 imp 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> t e. dom O )
86 fvco3 
 |-  ( ( O : dom O --> B /\ t e. dom O ) -> ( ( f o. O ) ` t ) = ( f ` ( O ` t ) ) )
87 21 85 86 syl2an2r 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` t ) = ( f ` ( O ` t ) ) )
88 simprl 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> s e. dom O )
89 fvco3 
 |-  ( ( O : dom O --> B /\ s e. dom O ) -> ( ( f o. O ) ` s ) = ( f ` ( O ` s ) ) )
90 21 88 89 syl2an2r 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` s ) = ( f ` ( O ` s ) ) )
91 81 87 90 3eltr4d 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ ( s e. dom O /\ t e. s ) ) -> ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) )
92 91 ralrimivva 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) )
93 issmo2 
 |-  ( ( f o. O ) : dom O --> A -> ( ( A C_ On /\ Ord dom O /\ A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) ) -> Smo ( f o. O ) ) )
94 93 imp 
 |-  ( ( ( f o. O ) : dom O --> A /\ ( A C_ On /\ Ord dom O /\ A. s e. dom O A. t e. s ( ( f o. O ) ` t ) e. ( ( f o. O ) ` s ) ) ) -> Smo ( f o. O ) )
95 50 52 53 92 94 syl13anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> Smo ( f o. O ) )
96 95 adantrr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> Smo ( f o. O ) )
97 rabn0 
 |-  ( { w e. B | z C_ ( f ` w ) } =/= (/) <-> E. w e. B z C_ ( f ` w ) )
98 ssrab2 
 |-  { w e. B | z C_ ( f ` w ) } C_ B
99 98 7 sstrid 
 |-  ( B e. On -> { w e. B | z C_ ( f ` w ) } C_ On )
100 fveq2 
 |-  ( x = w -> ( f ` x ) = ( f ` w ) )
101 100 sseq2d 
 |-  ( x = w -> ( z C_ ( f ` x ) <-> z C_ ( f ` w ) ) )
102 101 cbvrabv 
 |-  { x e. B | z C_ ( f ` x ) } = { w e. B | z C_ ( f ` w ) }
103 102 inteqi 
 |-  |^| { x e. B | z C_ ( f ` x ) } = |^| { w e. B | z C_ ( f ` w ) }
104 2 103 eqtri 
 |-  K = |^| { w e. B | z C_ ( f ` w ) }
105 onint 
 |-  ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> |^| { w e. B | z C_ ( f ` w ) } e. { w e. B | z C_ ( f ` w ) } )
106 104 105 eqeltrid 
 |-  ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> K e. { w e. B | z C_ ( f ` w ) } )
107 99 106 sylan 
 |-  ( ( B e. On /\ { w e. B | z C_ ( f ` w ) } =/= (/) ) -> K e. { w e. B | z C_ ( f ` w ) } )
108 97 107 sylan2br 
 |-  ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> K e. { w e. B | z C_ ( f ` w ) } )
109 fveq2 
 |-  ( w = K -> ( f ` w ) = ( f ` K ) )
110 109 sseq2d 
 |-  ( w = K -> ( z C_ ( f ` w ) <-> z C_ ( f ` K ) ) )
111 110 elrab 
 |-  ( K e. { w e. B | z C_ ( f ` w ) } <-> ( K e. B /\ z C_ ( f ` K ) ) )
112 108 111 sylib 
 |-  ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> ( K e. B /\ z C_ ( f ` K ) ) )
113 112 ex 
 |-  ( B e. On -> ( E. w e. B z C_ ( f ` w ) -> ( K e. B /\ z C_ ( f ` K ) ) ) )
114 113 adantl 
 |-  ( ( Ord A /\ B e. On ) -> ( E. w e. B z C_ ( f ` w ) -> ( K e. B /\ z C_ ( f ` K ) ) ) )
115 simpr2 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> K e. B )
116 simp3 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> w e. K )
117 104 eleq2i 
 |-  ( w e. K <-> w e. |^| { w e. B | z C_ ( f ` w ) } )
118 simp21 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> f : B --> A )
119 simp1l 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> Ord A )
120 119 51 syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> A C_ On )
121 118 120 fssd 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> f : B --> On )
122 simp22 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> K e. B )
123 121 122 ffvelcdmd 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` K ) e. On )
124 simp1r 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> B e. On )
125 ontr1 
 |-  ( B e. On -> ( ( w e. K /\ K e. B ) -> w e. B ) )
126 125 3impib 
 |-  ( ( B e. On /\ w e. K /\ K e. B ) -> w e. B )
127 124 116 122 126 syl3anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> w e. B )
128 121 127 ffvelcdmd 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` w ) e. On )
129 ontri1 
 |-  ( ( ( f ` K ) e. On /\ ( f ` w ) e. On ) -> ( ( f ` K ) C_ ( f ` w ) <-> -. ( f ` w ) e. ( f ` K ) ) )
130 123 128 129 syl2anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( ( f ` K ) C_ ( f ` w ) <-> -. ( f ` w ) e. ( f ` K ) ) )
131 simp23 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> z C_ ( f ` K ) )
132 simpl1 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> B e. On )
133 132 99 syl 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> { w e. B | z C_ ( f ` w ) } C_ On )
134 sstr 
 |-  ( ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) -> z C_ ( f ` w ) )
135 126 134 anim12i 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> ( w e. B /\ z C_ ( f ` w ) ) )
136 rabid 
 |-  ( w e. { w e. B | z C_ ( f ` w ) } <-> ( w e. B /\ z C_ ( f ` w ) ) )
137 135 136 sylibr 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> w e. { w e. B | z C_ ( f ` w ) } )
138 onnmin 
 |-  ( ( { w e. B | z C_ ( f ` w ) } C_ On /\ w e. { w e. B | z C_ ( f ` w ) } ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } )
139 133 137 138 syl2anc 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ ( z C_ ( f ` K ) /\ ( f ` K ) C_ ( f ` w ) ) ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } )
140 139 expr 
 |-  ( ( ( B e. On /\ w e. K /\ K e. B ) /\ z C_ ( f ` K ) ) -> ( ( f ` K ) C_ ( f ` w ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
141 124 116 122 131 140 syl31anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( ( f ` K ) C_ ( f ` w ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
142 130 141 sylbird 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( -. ( f ` w ) e. ( f ` K ) -> -. w e. |^| { w e. B | z C_ ( f ` w ) } ) )
143 142 con4d 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( w e. |^| { w e. B | z C_ ( f ` w ) } -> ( f ` w ) e. ( f ` K ) ) )
144 117 143 biimtrid 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( w e. K -> ( f ` w ) e. ( f ` K ) ) )
145 116 144 mpd 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) /\ w e. K ) -> ( f ` w ) e. ( f ` K ) )
146 145 3expia 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> ( w e. K -> ( f ` w ) e. ( f ` K ) ) )
147 146 ralrimiv 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> A. w e. K ( f ` w ) e. ( f ` K ) )
148 fveq2 
 |-  ( y = K -> ( f ` y ) = ( f ` K ) )
149 148 eleq2d 
 |-  ( y = K -> ( ( f ` w ) e. ( f ` y ) <-> ( f ` w ) e. ( f ` K ) ) )
150 149 raleqbi1dv 
 |-  ( y = K -> ( A. w e. y ( f ` w ) e. ( f ` y ) <-> A. w e. K ( f ` w ) e. ( f ` K ) ) )
151 150 1 elrab2 
 |-  ( K e. C <-> ( K e. B /\ A. w e. K ( f ` w ) e. ( f ` K ) ) )
152 115 147 151 sylanbrc 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) ) -> K e. C )
153 152 expcom 
 |-  ( ( f : B --> A /\ K e. B /\ z C_ ( f ` K ) ) -> ( ( Ord A /\ B e. On ) -> K e. C ) )
154 153 3expib 
 |-  ( f : B --> A -> ( ( K e. B /\ z C_ ( f ` K ) ) -> ( ( Ord A /\ B e. On ) -> K e. C ) ) )
155 154 com13 
 |-  ( ( Ord A /\ B e. On ) -> ( ( K e. B /\ z C_ ( f ` K ) ) -> ( f : B --> A -> K e. C ) ) )
156 114 155 syld 
 |-  ( ( Ord A /\ B e. On ) -> ( E. w e. B z C_ ( f ` w ) -> ( f : B --> A -> K e. C ) ) )
157 156 com23 
 |-  ( ( Ord A /\ B e. On ) -> ( f : B --> A -> ( E. w e. B z C_ ( f ` w ) -> K e. C ) ) )
158 157 imp31 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> K e. C )
159 foelrn 
 |-  ( ( O : dom O -onto-> C /\ K e. C ) -> E. v e. dom O K = ( O ` v ) )
160 17 158 159 syl2an2r 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> E. v e. dom O K = ( O ` v ) )
161 eleq1 
 |-  ( K = ( O ` v ) -> ( K e. { w e. B | z C_ ( f ` w ) } <-> ( O ` v ) e. { w e. B | z C_ ( f ` w ) } ) )
162 161 biimpcd 
 |-  ( K e. { w e. B | z C_ ( f ` w ) } -> ( K = ( O ` v ) -> ( O ` v ) e. { w e. B | z C_ ( f ` w ) } ) )
163 fveq2 
 |-  ( x = ( O ` v ) -> ( f ` x ) = ( f ` ( O ` v ) ) )
164 163 sseq2d 
 |-  ( x = ( O ` v ) -> ( z C_ ( f ` x ) <-> z C_ ( f ` ( O ` v ) ) ) )
165 66 sseq2d 
 |-  ( w = x -> ( z C_ ( f ` w ) <-> z C_ ( f ` x ) ) )
166 165 cbvrabv 
 |-  { w e. B | z C_ ( f ` w ) } = { x e. B | z C_ ( f ` x ) }
167 164 166 elrab2 
 |-  ( ( O ` v ) e. { w e. B | z C_ ( f ` w ) } <-> ( ( O ` v ) e. B /\ z C_ ( f ` ( O ` v ) ) ) )
168 167 simprbi 
 |-  ( ( O ` v ) e. { w e. B | z C_ ( f ` w ) } -> z C_ ( f ` ( O ` v ) ) )
169 162 168 syl6 
 |-  ( K e. { w e. B | z C_ ( f ` w ) } -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
170 108 169 syl 
 |-  ( ( B e. On /\ E. w e. B z C_ ( f ` w ) ) -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
171 170 ad5ant24 
 |-  ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( K = ( O ` v ) -> z C_ ( f ` ( O ` v ) ) ) )
172 21 ad2antrr 
 |-  ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> O : dom O --> B )
173 fvco3 
 |-  ( ( O : dom O --> B /\ v e. dom O ) -> ( ( f o. O ) ` v ) = ( f ` ( O ` v ) ) )
174 172 173 sylancom 
 |-  ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( ( f o. O ) ` v ) = ( f ` ( O ` v ) ) )
175 174 sseq2d 
 |-  ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( z C_ ( ( f o. O ) ` v ) <-> z C_ ( f ` ( O ` v ) ) ) )
176 171 175 sylibrd 
 |-  ( ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) /\ v e. dom O ) -> ( K = ( O ` v ) -> z C_ ( ( f o. O ) ` v ) ) )
177 176 reximdva 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> ( E. v e. dom O K = ( O ` v ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
178 160 177 mpd 
 |-  ( ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) /\ E. w e. B z C_ ( f ` w ) ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) )
179 178 ex 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( E. w e. B z C_ ( f ` w ) -> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
180 179 ralimdv 
 |-  ( ( ( Ord A /\ B e. On ) /\ f : B --> A ) -> ( A. z e. A E. w e. B z C_ ( f ` w ) -> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
181 180 impr 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) )
182 48 96 181 3jca 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> ( ( f o. O ) : dom O --> A /\ Smo ( f o. O ) /\ A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
183 feq1 
 |-  ( g = ( f o. O ) -> ( g : dom O --> A <-> ( f o. O ) : dom O --> A ) )
184 smoeq 
 |-  ( g = ( f o. O ) -> ( Smo g <-> Smo ( f o. O ) ) )
185 fveq1 
 |-  ( g = ( f o. O ) -> ( g ` v ) = ( ( f o. O ) ` v ) )
186 185 sseq2d 
 |-  ( g = ( f o. O ) -> ( z C_ ( g ` v ) <-> z C_ ( ( f o. O ) ` v ) ) )
187 186 rexbidv 
 |-  ( g = ( f o. O ) -> ( E. v e. dom O z C_ ( g ` v ) <-> E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
188 187 ralbidv 
 |-  ( g = ( f o. O ) -> ( A. z e. A E. v e. dom O z C_ ( g ` v ) <-> A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) )
189 183 184 188 3anbi123d 
 |-  ( g = ( f o. O ) -> ( ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) <-> ( ( f o. O ) : dom O --> A /\ Smo ( f o. O ) /\ A. z e. A E. v e. dom O z C_ ( ( f o. O ) ` v ) ) ) )
190 45 182 189 spcedv 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) )
191 feq2 
 |-  ( x = dom O -> ( g : x --> A <-> g : dom O --> A ) )
192 rexeq 
 |-  ( x = dom O -> ( E. v e. x z C_ ( g ` v ) <-> E. v e. dom O z C_ ( g ` v ) ) )
193 192 ralbidv 
 |-  ( x = dom O -> ( A. z e. A E. v e. x z C_ ( g ` v ) <-> A. z e. A E. v e. dom O z C_ ( g ` v ) ) )
194 191 193 3anbi13d 
 |-  ( x = dom O -> ( ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) <-> ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) )
195 194 exbidv 
 |-  ( x = dom O -> ( E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) <-> E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) )
196 195 rspcev 
 |-  ( ( dom O e. suc B /\ E. g ( g : dom O --> A /\ Smo g /\ A. z e. A E. v e. dom O z C_ ( g ` v ) ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) )
197 39 190 196 syl2anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) )
198 197 ex 
 |-  ( ( Ord A /\ B e. On ) -> ( ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )
199 198 exlimdv 
 |-  ( ( Ord A /\ B e. On ) -> ( E. f ( f : B --> A /\ A. z e. A E. w e. B z C_ ( f ` w ) ) -> E. x e. suc B E. g ( g : x --> A /\ Smo g /\ A. z e. A E. v e. x z C_ ( g ` v ) ) ) )