Metamath Proof Explorer

Theorem bndth

Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -u F .) (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 
|- X = U. J
bndth.2 
|- K = ( topGen ` ran (,) )
bndth.3 
|- ( ph -> J e. Comp )
bndth.4 
|- ( ph -> F e. ( J Cn K ) )
Assertion bndth 
|- ( ph -> E. x e. RR A. y e. X ( F ` y ) <_ x )

Proof

Step Hyp Ref Expression
1 bndth.1 
 |-  X = U. J
2 bndth.2 
 |-  K = ( topGen ` ran (,) )
3 bndth.3 
 |-  ( ph -> J e. Comp )
4 bndth.4 
 |-  ( ph -> F e. ( J Cn K ) )
5 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
6 2 5 eqeltri 
 |-  K e. ( TopOn ` RR )
7 6 toponunii 
 |-  RR = U. K
8 1 7 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> RR )
9 4 8 syl 
 |-  ( ph -> F : X --> RR )
10 9 frnd 
 |-  ( ph -> ran F C_ RR )
11 unieq 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> U. u = U. ( (,) " ( { -oo } X. RR ) ) )
12 imassrn 
 |-  ( (,) " ( { -oo } X. RR ) ) C_ ran (,)
13 12 unissi 
 |-  U. ( (,) " ( { -oo } X. RR ) ) C_ U. ran (,)
14 unirnioo 
 |-  RR = U. ran (,)
15 13 14 sseqtrri 
 |-  U. ( (,) " ( { -oo } X. RR ) ) C_ RR
16 id 
 |-  ( x e. RR -> x e. RR )
17 ltp1 
 |-  ( x e. RR -> x < ( x + 1 ) )
18 ressxr 
 |-  RR C_ RR*
19 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
20 18 19 sselid 
 |-  ( x e. RR -> ( x + 1 ) e. RR* )
21 elioomnf 
 |-  ( ( x + 1 ) e. RR* -> ( x e. ( -oo (,) ( x + 1 ) ) <-> ( x e. RR /\ x < ( x + 1 ) ) ) )
22 20 21 syl 
 |-  ( x e. RR -> ( x e. ( -oo (,) ( x + 1 ) ) <-> ( x e. RR /\ x < ( x + 1 ) ) ) )
23 16 17 22 mpbir2and 
 |-  ( x e. RR -> x e. ( -oo (,) ( x + 1 ) ) )
24 df-ov 
 |-  ( -oo (,) ( x + 1 ) ) = ( (,) ` <. -oo , ( x + 1 ) >. )
25 mnfxr 
 |-  -oo e. RR*
26 25 elexi 
 |-  -oo e. _V
27 26 snid 
 |-  -oo e. { -oo }
28 opelxpi 
 |-  ( ( -oo e. { -oo } /\ ( x + 1 ) e. RR ) -> <. -oo , ( x + 1 ) >. e. ( { -oo } X. RR ) )
29 27 19 28 sylancr 
 |-  ( x e. RR -> <. -oo , ( x + 1 ) >. e. ( { -oo } X. RR ) )
30 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
31 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
32 30 31 ax-mp 
 |-  Fun (,)
33 snssi 
 |-  ( -oo e. RR* -> { -oo } C_ RR* )
34 25 33 ax-mp 
 |-  { -oo } C_ RR*
35 xpss12 
 |-  ( ( { -oo } C_ RR* /\ RR C_ RR* ) -> ( { -oo } X. RR ) C_ ( RR* X. RR* ) )
36 34 18 35 mp2an 
 |-  ( { -oo } X. RR ) C_ ( RR* X. RR* )
37 30 fdmi 
 |-  dom (,) = ( RR* X. RR* )
38 36 37 sseqtrri 
 |-  ( { -oo } X. RR ) C_ dom (,)
39 funfvima2 
 |-  ( ( Fun (,) /\ ( { -oo } X. RR ) C_ dom (,) ) -> ( <. -oo , ( x + 1 ) >. e. ( { -oo } X. RR ) -> ( (,) ` <. -oo , ( x + 1 ) >. ) e. ( (,) " ( { -oo } X. RR ) ) ) )
40 32 38 39 mp2an 
 |-  ( <. -oo , ( x + 1 ) >. e. ( { -oo } X. RR ) -> ( (,) ` <. -oo , ( x + 1 ) >. ) e. ( (,) " ( { -oo } X. RR ) ) )
41 29 40 syl 
 |-  ( x e. RR -> ( (,) ` <. -oo , ( x + 1 ) >. ) e. ( (,) " ( { -oo } X. RR ) ) )
42 24 41 eqeltrid 
 |-  ( x e. RR -> ( -oo (,) ( x + 1 ) ) e. ( (,) " ( { -oo } X. RR ) ) )
43 elunii 
 |-  ( ( x e. ( -oo (,) ( x + 1 ) ) /\ ( -oo (,) ( x + 1 ) ) e. ( (,) " ( { -oo } X. RR ) ) ) -> x e. U. ( (,) " ( { -oo } X. RR ) ) )
44 23 42 43 syl2anc 
 |-  ( x e. RR -> x e. U. ( (,) " ( { -oo } X. RR ) ) )
45 44 ssriv 
 |-  RR C_ U. ( (,) " ( { -oo } X. RR ) )
46 15 45 eqssi 
 |-  U. ( (,) " ( { -oo } X. RR ) ) = RR
47 11 46 eqtrdi 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> U. u = RR )
48 47 sseq2d 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> ( ran F C_ U. u <-> ran F C_ RR ) )
49 pweq 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> ~P u = ~P ( (,) " ( { -oo } X. RR ) ) )
50 49 ineq1d 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> ( ~P u i^i Fin ) = ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) )
51 50 rexeqdv 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> ( E. v e. ( ~P u i^i Fin ) ran F C_ U. v <-> E. v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ran F C_ U. v ) )
52 48 51 imbi12d 
 |-  ( u = ( (,) " ( { -oo } X. RR ) ) -> ( ( ran F C_ U. u -> E. v e. ( ~P u i^i Fin ) ran F C_ U. v ) <-> ( ran F C_ RR -> E. v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ran F C_ U. v ) ) )
53 rncmp 
 |-  ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( K |`t ran F ) e. Comp )
54 3 4 53 syl2anc 
 |-  ( ph -> ( K |`t ran F ) e. Comp )
55 retop 
 |-  ( topGen ` ran (,) ) e. Top
56 2 55 eqeltri 
 |-  K e. Top
57 7 cmpsub 
 |-  ( ( K e. Top /\ ran F C_ RR ) -> ( ( K |`t ran F ) e. Comp <-> A. u e. ~P K ( ran F C_ U. u -> E. v e. ( ~P u i^i Fin ) ran F C_ U. v ) ) )
58 56 10 57 sylancr 
 |-  ( ph -> ( ( K |`t ran F ) e. Comp <-> A. u e. ~P K ( ran F C_ U. u -> E. v e. ( ~P u i^i Fin ) ran F C_ U. v ) ) )
59 54 58 mpbid 
 |-  ( ph -> A. u e. ~P K ( ran F C_ U. u -> E. v e. ( ~P u i^i Fin ) ran F C_ U. v ) )
60 retopbas 
 |-  ran (,) e. TopBases
61 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
62 60 61 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
63 62 2 sseqtrri 
 |-  ran (,) C_ K
64 12 63 sstri 
 |-  ( (,) " ( { -oo } X. RR ) ) C_ K
65 56 64 elpwi2 
 |-  ( (,) " ( { -oo } X. RR ) ) e. ~P K
66 65 a1i 
 |-  ( ph -> ( (,) " ( { -oo } X. RR ) ) e. ~P K )
67 52 59 66 rspcdva 
 |-  ( ph -> ( ran F C_ RR -> E. v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ran F C_ U. v ) )
68 10 67 mpd 
 |-  ( ph -> E. v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ran F C_ U. v )
69 elin 
 |-  ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) <-> ( v e. ~P ( (,) " ( { -oo } X. RR ) ) /\ v e. Fin ) )
70 69 bilani 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> ( v e. ~P ( (,) " ( { -oo } X. RR ) ) /\ v e. Fin ) )
71 70 adantrr 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> ( v e. ~P ( (,) " ( { -oo } X. RR ) ) /\ v e. Fin ) )
72 71 simprd 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> v e. Fin )
73 70 simpld 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> v e. ~P ( (,) " ( { -oo } X. RR ) ) )
74 73 elpwid 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> v C_ ( (,) " ( { -oo } X. RR ) ) )
75 34 sseli 
 |-  ( u e. { -oo } -> u e. RR* )
76 75 adantr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> u e. RR* )
77 18 sseli 
 |-  ( w e. RR -> w e. RR* )
78 77 adantl 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> w e. RR* )
79 mnflt 
 |-  ( w e. RR -> -oo < w )
80 xrltnle 
 |-  ( ( -oo e. RR* /\ w e. RR* ) -> ( -oo < w <-> -. w <_ -oo ) )
81 25 77 80 sylancr 
 |-  ( w e. RR -> ( -oo < w <-> -. w <_ -oo ) )
82 79 81 mpbid 
 |-  ( w e. RR -> -. w <_ -oo )
83 82 adantl 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> -. w <_ -oo )
84 elsni 
 |-  ( u e. { -oo } -> u = -oo )
85 84 adantr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> u = -oo )
86 85 breq2d 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( w <_ u <-> w <_ -oo ) )
87 83 86 mtbird 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> -. w <_ u )
88 ioo0 
 |-  ( ( u e. RR* /\ w e. RR* ) -> ( ( u (,) w ) = (/) <-> w <_ u ) )
89 75 77 88 syl2an 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( ( u (,) w ) = (/) <-> w <_ u ) )
90 89 necon3abid 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( ( u (,) w ) =/= (/) <-> -. w <_ u ) )
91 87 90 mpbird 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( u (,) w ) =/= (/) )
92 df-ioo 
 |-  (,) = ( y e. RR* , z e. RR* |-> { v e. RR* | ( y < v /\ v < z ) } )
93 idd 
 |-  ( ( x e. RR* /\ w e. RR* ) -> ( x < w -> x < w ) )
94 xrltle 
 |-  ( ( x e. RR* /\ w e. RR* ) -> ( x < w -> x <_ w ) )
95 idd 
 |-  ( ( u e. RR* /\ x e. RR* ) -> ( u < x -> u < x ) )
96 xrltle 
 |-  ( ( u e. RR* /\ x e. RR* ) -> ( u < x -> u <_ x ) )
97 92 93 94 95 96 ixxub 
 |-  ( ( u e. RR* /\ w e. RR* /\ ( u (,) w ) =/= (/) ) -> sup ( ( u (,) w ) , RR* , < ) = w )
98 76 78 91 97 syl3anc 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> sup ( ( u (,) w ) , RR* , < ) = w )
99 simpr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> w e. RR )
100 98 99 eqeltrd 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> sup ( ( u (,) w ) , RR* , < ) e. RR )
101 100 rgen2 
 |-  A. u e. { -oo } A. w e. RR sup ( ( u (,) w ) , RR* , < ) e. RR
102 fveq2 
 |-  ( z = <. u , w >. -> ( (,) ` z ) = ( (,) ` <. u , w >. ) )
103 df-ov 
 |-  ( u (,) w ) = ( (,) ` <. u , w >. )
104 102 103 eqtr4di 
 |-  ( z = <. u , w >. -> ( (,) ` z ) = ( u (,) w ) )
105 104 supeq1d 
 |-  ( z = <. u , w >. -> sup ( ( (,) ` z ) , RR* , < ) = sup ( ( u (,) w ) , RR* , < ) )
106 105 eleq1d 
 |-  ( z = <. u , w >. -> ( sup ( ( (,) ` z ) , RR* , < ) e. RR <-> sup ( ( u (,) w ) , RR* , < ) e. RR ) )
107 106 ralxp 
 |-  ( A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR <-> A. u e. { -oo } A. w e. RR sup ( ( u (,) w ) , RR* , < ) e. RR )
108 101 107 mpbir 
 |-  A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR
109 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
110 30 109 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
111 supeq1 
 |-  ( w = ( (,) ` z ) -> sup ( w , RR* , < ) = sup ( ( (,) ` z ) , RR* , < ) )
112 111 eleq1d 
 |-  ( w = ( (,) ` z ) -> ( sup ( w , RR* , < ) e. RR <-> sup ( ( (,) ` z ) , RR* , < ) e. RR ) )
113 112 ralima 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( { -oo } X. RR ) C_ ( RR* X. RR* ) ) -> ( A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR <-> A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR ) )
114 110 36 113 mp2an 
 |-  ( A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR <-> A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR )
115 108 114 mpbir 
 |-  A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR
116 ssralv 
 |-  ( v C_ ( (,) " ( { -oo } X. RR ) ) -> ( A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR -> A. w e. v sup ( w , RR* , < ) e. RR ) )
117 74 115 116 mpisyl 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> A. w e. v sup ( w , RR* , < ) e. RR )
118 117 adantrr 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> A. w e. v sup ( w , RR* , < ) e. RR )
119 fimaxre3 
 |-  ( ( v e. Fin /\ A. w e. v sup ( w , RR* , < ) e. RR ) -> E. x e. RR A. w e. v sup ( w , RR* , < ) <_ x )
120 72 118 119 syl2anc 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> E. x e. RR A. w e. v sup ( w , RR* , < ) <_ x )
121 simplrr 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ran F C_ U. v )
122 121 sselda 
 |-  ( ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) /\ z e. ran F ) -> z e. U. v )
123 eluni2 
 |-  ( z e. U. v <-> E. w e. v z e. w )
124 r19.29r 
 |-  ( ( E. w e. v z e. w /\ A. w e. v sup ( w , RR* , < ) <_ x ) -> E. w e. v ( z e. w /\ sup ( w , RR* , < ) <_ x ) )
125 sspwuni 
 |-  ( ( (,) " ( { -oo } X. RR ) ) C_ ~P RR <-> U. ( (,) " ( { -oo } X. RR ) ) C_ RR )
126 15 125 mpbir 
 |-  ( (,) " ( { -oo } X. RR ) ) C_ ~P RR
127 74 3ad2ant1 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> v C_ ( (,) " ( { -oo } X. RR ) ) )
128 simp2r 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> w e. v )
129 127 128 sseldd 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> w e. ( (,) " ( { -oo } X. RR ) ) )
130 126 129 sselid 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> w e. ~P RR )
131 130 elpwid 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> w C_ RR )
132 simp3l 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> z e. w )
133 131 132 sseldd 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> z e. RR )
134 117 r19.21bi 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ w e. v ) -> sup ( w , RR* , < ) e. RR )
135 134 adantrl 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) ) -> sup ( w , RR* , < ) e. RR )
136 135 3adant3 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> sup ( w , RR* , < ) e. RR )
137 simp2l 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> x e. RR )
138 131 18 sstrdi 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> w C_ RR* )
139 supxrub 
 |-  ( ( w C_ RR* /\ z e. w ) -> z <_ sup ( w , RR* , < ) )
140 138 132 139 syl2anc 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> z <_ sup ( w , RR* , < ) )
141 simp3r 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> sup ( w , RR* , < ) <_ x )
142 133 136 137 140 141 letrd 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) /\ ( z e. w /\ sup ( w , RR* , < ) <_ x ) ) -> z <_ x )
143 142 3expia 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) ) -> ( ( z e. w /\ sup ( w , RR* , < ) <_ x ) -> z <_ x ) )
144 143 anassrs 
 |-  ( ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ x e. RR ) /\ w e. v ) -> ( ( z e. w /\ sup ( w , RR* , < ) <_ x ) -> z <_ x ) )
145 144 rexlimdva 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ x e. RR ) -> ( E. w e. v ( z e. w /\ sup ( w , RR* , < ) <_ x ) -> z <_ x ) )
146 145 adantlrr 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ( E. w e. v ( z e. w /\ sup ( w , RR* , < ) <_ x ) -> z <_ x ) )
147 124 146 syl5 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ( ( E. w e. v z e. w /\ A. w e. v sup ( w , RR* , < ) <_ x ) -> z <_ x ) )
148 147 expdimp 
 |-  ( ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) /\ E. w e. v z e. w ) -> ( A. w e. v sup ( w , RR* , < ) <_ x -> z <_ x ) )
149 123 148 sylan2b 
 |-  ( ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) /\ z e. U. v ) -> ( A. w e. v sup ( w , RR* , < ) <_ x -> z <_ x ) )
150 122 149 syldan 
 |-  ( ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) /\ z e. ran F ) -> ( A. w e. v sup ( w , RR* , < ) <_ x -> z <_ x ) )
151 150 ralrimdva 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ( A. w e. v sup ( w , RR* , < ) <_ x -> A. z e. ran F z <_ x ) )
152 9 ffnd 
 |-  ( ph -> F Fn X )
153 152 ad2antrr 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> F Fn X )
154 breq1 
 |-  ( z = ( F ` y ) -> ( z <_ x <-> ( F ` y ) <_ x ) )
155 154 ralrn 
 |-  ( F Fn X -> ( A. z e. ran F z <_ x <-> A. y e. X ( F ` y ) <_ x ) )
156 153 155 syl 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ( A. z e. ran F z <_ x <-> A. y e. X ( F ` y ) <_ x ) )
157 151 156 sylibd 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ( A. w e. v sup ( w , RR* , < ) <_ x -> A. y e. X ( F ` y ) <_ x ) )
158 157 reximdva 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> ( E. x e. RR A. w e. v sup ( w , RR* , < ) <_ x -> E. x e. RR A. y e. X ( F ` y ) <_ x ) )
159 120 158 mpd 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> E. x e. RR A. y e. X ( F ` y ) <_ x )
160 68 159 rexlimddv 
 |-  ( ph -> E. x e. RR A. y e. X ( F ` y ) <_ x )