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 simpr 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) )
70 elin 
 |-  ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) <-> ( v e. ~P ( (,) " ( { -oo } X. RR ) ) /\ v e. Fin ) )
71 69 70 sylib 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> ( v e. ~P ( (,) " ( { -oo } X. RR ) ) /\ v e. Fin ) )
72 71 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 ) )
73 72 simprd 
 |-  ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) -> v e. Fin )
74 71 simpld 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> v e. ~P ( (,) " ( { -oo } X. RR ) ) )
75 74 elpwid 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> v C_ ( (,) " ( { -oo } X. RR ) ) )
76 34 sseli 
 |-  ( u e. { -oo } -> u e. RR* )
77 76 adantr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> u e. RR* )
78 18 sseli 
 |-  ( w e. RR -> w e. RR* )
79 78 adantl 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> w e. RR* )
80 mnflt 
 |-  ( w e. RR -> -oo < w )
81 xrltnle 
 |-  ( ( -oo e. RR* /\ w e. RR* ) -> ( -oo < w <-> -. w <_ -oo ) )
82 25 78 81 sylancr 
 |-  ( w e. RR -> ( -oo < w <-> -. w <_ -oo ) )
83 80 82 mpbid 
 |-  ( w e. RR -> -. w <_ -oo )
84 83 adantl 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> -. w <_ -oo )
85 elsni 
 |-  ( u e. { -oo } -> u = -oo )
86 85 adantr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> u = -oo )
87 86 breq2d 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( w <_ u <-> w <_ -oo ) )
88 84 87 mtbird 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> -. w <_ u )
89 ioo0 
 |-  ( ( u e. RR* /\ w e. RR* ) -> ( ( u (,) w ) = (/) <-> w <_ u ) )
90 76 78 89 syl2an 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( ( u (,) w ) = (/) <-> w <_ u ) )
91 90 necon3abid 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( ( u (,) w ) =/= (/) <-> -. w <_ u ) )
92 88 91 mpbird 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> ( u (,) w ) =/= (/) )
93 df-ioo 
 |-  (,) = ( y e. RR* , z e. RR* |-> { v e. RR* | ( y < v /\ v < z ) } )
94 idd 
 |-  ( ( x e. RR* /\ w e. RR* ) -> ( x < w -> x < w ) )
95 xrltle 
 |-  ( ( x e. RR* /\ w e. RR* ) -> ( x < w -> x <_ w ) )
96 idd 
 |-  ( ( u e. RR* /\ x e. RR* ) -> ( u < x -> u < x ) )
97 xrltle 
 |-  ( ( u e. RR* /\ x e. RR* ) -> ( u < x -> u <_ x ) )
98 93 94 95 96 97 ixxub 
 |-  ( ( u e. RR* /\ w e. RR* /\ ( u (,) w ) =/= (/) ) -> sup ( ( u (,) w ) , RR* , < ) = w )
99 77 79 92 98 syl3anc 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> sup ( ( u (,) w ) , RR* , < ) = w )
100 simpr 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> w e. RR )
101 99 100 eqeltrd 
 |-  ( ( u e. { -oo } /\ w e. RR ) -> sup ( ( u (,) w ) , RR* , < ) e. RR )
102 101 rgen2 
 |-  A. u e. { -oo } A. w e. RR sup ( ( u (,) w ) , RR* , < ) e. RR
103 fveq2 
 |-  ( z = <. u , w >. -> ( (,) ` z ) = ( (,) ` <. u , w >. ) )
104 df-ov 
 |-  ( u (,) w ) = ( (,) ` <. u , w >. )
105 103 104 eqtr4di 
 |-  ( z = <. u , w >. -> ( (,) ` z ) = ( u (,) w ) )
106 105 supeq1d 
 |-  ( z = <. u , w >. -> sup ( ( (,) ` z ) , RR* , < ) = sup ( ( u (,) w ) , RR* , < ) )
107 106 eleq1d 
 |-  ( z = <. u , w >. -> ( sup ( ( (,) ` z ) , RR* , < ) e. RR <-> sup ( ( u (,) w ) , RR* , < ) e. RR ) )
108 107 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 )
109 102 108 mpbir 
 |-  A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR
110 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
111 30 110 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
112 supeq1 
 |-  ( w = ( (,) ` z ) -> sup ( w , RR* , < ) = sup ( ( (,) ` z ) , RR* , < ) )
113 112 eleq1d 
 |-  ( w = ( (,) ` z ) -> ( sup ( w , RR* , < ) e. RR <-> sup ( ( (,) ` z ) , RR* , < ) e. RR ) )
114 113 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 ) )
115 111 36 114 mp2an 
 |-  ( A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR <-> A. z e. ( { -oo } X. RR ) sup ( ( (,) ` z ) , RR* , < ) e. RR )
116 109 115 mpbir 
 |-  A. w e. ( (,) " ( { -oo } X. RR ) ) sup ( w , RR* , < ) e. RR
117 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 ) )
118 75 116 117 mpisyl 
 |-  ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) -> A. w e. v sup ( w , RR* , < ) e. RR )
119 118 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 )
120 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 )
121 73 119 120 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 )
122 simplrr 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> ran F C_ U. v )
123 122 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 )
124 eluni2 
 |-  ( z e. U. v <-> E. w e. v z e. w )
125 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 ) )
126 sspwuni 
 |-  ( ( (,) " ( { -oo } X. RR ) ) C_ ~P RR <-> U. ( (,) " ( { -oo } X. RR ) ) C_ RR )
127 15 126 mpbir 
 |-  ( (,) " ( { -oo } X. RR ) ) C_ ~P RR
128 75 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 ) ) )
129 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 )
130 128 129 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 ) ) )
131 127 130 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 )
132 131 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 )
133 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 )
134 132 133 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 )
135 118 r19.21bi 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ w e. v ) -> sup ( w , RR* , < ) e. RR )
136 135 adantrl 
 |-  ( ( ( ph /\ v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) ) /\ ( x e. RR /\ w e. v ) ) -> sup ( w , RR* , < ) e. RR )
137 136 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 )
138 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 )
139 132 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* )
140 supxrub 
 |-  ( ( w C_ RR* /\ z e. w ) -> z <_ sup ( w , RR* , < ) )
141 139 133 140 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* , < ) )
142 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 )
143 134 137 138 141 142 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 )
144 143 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 ) )
145 144 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 ) )
146 145 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 ) )
147 146 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 ) )
148 125 147 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 ) )
149 148 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 ) )
150 124 149 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 ) )
151 123 150 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 ) )
152 151 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 ) )
153 9 ffnd 
 |-  ( ph -> F Fn X )
154 153 ad2antrr 
 |-  ( ( ( ph /\ ( v e. ( ~P ( (,) " ( { -oo } X. RR ) ) i^i Fin ) /\ ran F C_ U. v ) ) /\ x e. RR ) -> F Fn X )
155 breq1 
 |-  ( z = ( F ` y ) -> ( z <_ x <-> ( F ` y ) <_ x ) )
156 155 ralrn 
 |-  ( F Fn X -> ( A. z e. ran F z <_ x <-> A. y e. X ( F ` y ) <_ x ) )
157 154 156 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 ) )
158 152 157 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 ) )
159 158 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 ) )
160 121 159 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 )
161 68 160 rexlimddv 
 |-  ( ph -> E. x e. RR A. y e. X ( F ` y ) <_ x )