Metamath Proof Explorer

Theorem ivthALT

Description: An alternate proof of the Intermediate Value Theorem ivth using topology. (Contributed by Jeff Hankins, 17-Aug-2009) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ivthALT 
|- ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> E. x e. ( A (,) B ) ( F ` x ) = U )

Proof

Step Hyp Ref Expression
1 simp31 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> F e. ( D -cn-> CC ) )
2 cncff 
 |-  ( F e. ( D -cn-> CC ) -> F : D --> CC )
3 1 2 syl 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> F : D --> CC )
4 ffun 
 |-  ( F : D --> CC -> Fun F )
5 3 4 syl 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> Fun F )
6 5 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> Fun F )
7 iccconn 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )
8 7 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ U e. RR ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )
9 8 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn )
10 simpr1 
 |-  ( ( D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> F e. ( D -cn-> CC ) )
11 10 2 syl 
 |-  ( ( D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> F : D --> CC )
12 11 anim2i 
 |-  ( ( ( A [,] B ) C_ D /\ ( D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( A [,] B ) C_ D /\ F : D --> CC ) )
13 12 3impb 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> ( ( A [,] B ) C_ D /\ F : D --> CC ) )
14 13 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( A [,] B ) C_ D /\ F : D --> CC ) )
15 4 adantl 
 |-  ( ( ( A [,] B ) C_ D /\ F : D --> CC ) -> Fun F )
16 fdm 
 |-  ( F : D --> CC -> dom F = D )
17 16 sseq2d 
 |-  ( F : D --> CC -> ( ( A [,] B ) C_ dom F <-> ( A [,] B ) C_ D ) )
18 17 biimparc 
 |-  ( ( ( A [,] B ) C_ D /\ F : D --> CC ) -> ( A [,] B ) C_ dom F )
19 15 18 jca 
 |-  ( ( ( A [,] B ) C_ D /\ F : D --> CC ) -> ( Fun F /\ ( A [,] B ) C_ dom F ) )
20 14 19 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( Fun F /\ ( A [,] B ) C_ dom F ) )
21 fores 
 |-  ( ( Fun F /\ ( A [,] B ) C_ dom F ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> ( F " ( A [,] B ) ) )
22 20 21 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> ( F " ( A [,] B ) ) )
23 retop 
 |-  ( topGen ` ran (,) ) e. Top
24 simp332 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F " ( A [,] B ) ) C_ RR )
25 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
26 25 restuni 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( F " ( A [,] B ) ) C_ RR ) -> ( F " ( A [,] B ) ) = U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) )
27 23 24 26 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F " ( A [,] B ) ) = U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) )
28 foeq3 
 |-  ( ( F " ( A [,] B ) ) = U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> ( F " ( A [,] B ) ) <-> ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) ) )
29 27 28 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> ( F " ( A [,] B ) ) <-> ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) ) )
30 22 29 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) )
31 simp331 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> F e. ( D -cn-> CC ) )
32 ssid 
 |-  CC C_ CC
33 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
34 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t D ) = ( ( TopOpen ` CCfld ) |`t D )
35 33 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
36 33 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
37 36 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
38 37 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
39 35 38 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
40 39 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
41 33 34 40 cncfcn 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
42 32 41 mpan2 
 |-  ( D C_ CC -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
43 42 3ad2ant2 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
44 43 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( D -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
45 31 44 eleqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> F e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) )
46 simp31 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( A [,] B ) C_ D )
47 simp32 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> D C_ CC )
48 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ D C_ CC ) -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
49 36 47 48 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) )
50 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t D ) e. ( TopOn ` D ) -> D = U. ( ( TopOpen ` CCfld ) |`t D ) )
51 49 50 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> D = U. ( ( TopOpen ` CCfld ) |`t D ) )
52 46 51 sseqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( A [,] B ) C_ U. ( ( TopOpen ` CCfld ) |`t D ) )
53 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t D ) = U. ( ( TopOpen ` CCfld ) |`t D )
54 53 cnrest 
 |-  ( ( F e. ( ( ( TopOpen ` CCfld ) |`t D ) Cn ( TopOpen ` CCfld ) ) /\ ( A [,] B ) C_ U. ( ( TopOpen ` CCfld ) |`t D ) ) -> ( F |` ( A [,] B ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
55 45 52 54 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
56 35 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( TopOpen ` CCfld ) e. Top )
57 cnex 
 |-  CC e. _V
58 ssexg 
 |-  ( ( D C_ CC /\ CC e. _V ) -> D e. _V )
59 47 57 58 sylancl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> D e. _V )
60 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A [,] B ) C_ D /\ D e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
61 56 46 59 60 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
62 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
63 62 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ U e. RR ) -> ( A [,] B ) C_ RR )
64 63 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( A [,] B ) C_ RR )
65 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
66 33 65 rerest 
 |-  ( ( A [,] B ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
67 64 66 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
68 61 67 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
69 68 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t D ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) = ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
70 55 69 eleqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
71 36 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
72 df-ima 
 |-  ( F " ( A [,] B ) ) = ran ( F |` ( A [,] B ) )
73 72 eqimss2i 
 |-  ran ( F |` ( A [,] B ) ) C_ ( F " ( A [,] B ) )
74 73 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ran ( F |` ( A [,] B ) ) C_ ( F " ( A [,] B ) ) )
75 ax-resscn 
 |-  RR C_ CC
76 24 75 sstrdi 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F " ( A [,] B ) ) C_ CC )
77 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( F |` ( A [,] B ) ) C_ ( F " ( A [,] B ) ) /\ ( F " ( A [,] B ) ) C_ CC ) -> ( ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) ) ) )
78 71 74 76 77 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) ) ) )
79 70 78 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) ) )
80 33 65 rerest 
 |-  ( ( F " ( A [,] B ) ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) = ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) )
81 24 80 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) = ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) )
82 81 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( TopOpen ` CCfld ) |`t ( F " ( A [,] B ) ) ) ) = ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) ) )
83 79 82 eleqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) ) )
84 eqid 
 |-  U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) = U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) )
85 84 cnconn 
 |-  ( ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) e. Conn /\ ( F |` ( A [,] B ) ) : ( A [,] B ) -onto-> U. ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) /\ ( F |` ( A [,] B ) ) e. ( ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) Cn ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) ) ) -> ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn )
86 9 30 83 85 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn )
87 reconn 
 |-  ( ( F " ( A [,] B ) ) C_ RR -> ( ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn <-> A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) ) )
88 87 3ad2ant2 
 |-  ( ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) -> ( ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn <-> A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) ) )
89 88 3ad2ant3 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> ( ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn <-> A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) ) )
90 89 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( topGen ` ran (,) ) |`t ( F " ( A [,] B ) ) ) e. Conn <-> A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) ) )
91 86 90 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) )
92 simp11 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> A e. RR )
93 92 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> A e. RR* )
94 simp12 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> B e. RR )
95 94 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> B e. RR* )
96 ltle 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
97 96 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A <_ B )
98 97 3adantl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B ) -> A <_ B )
99 98 3adant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> A <_ B )
100 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
101 93 95 99 100 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> A e. ( A [,] B ) )
102 funfvima2 
 |-  ( ( Fun F /\ ( A [,] B ) C_ dom F ) -> ( A e. ( A [,] B ) -> ( F ` A ) e. ( F " ( A [,] B ) ) ) )
103 20 101 102 sylc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` A ) e. ( F " ( A [,] B ) ) )
104 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
105 93 95 99 104 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> B e. ( A [,] B ) )
106 funfvima2 
 |-  ( ( Fun F /\ ( A [,] B ) C_ dom F ) -> ( B e. ( A [,] B ) -> ( F ` B ) e. ( F " ( A [,] B ) ) ) )
107 20 105 106 sylc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` B ) e. ( F " ( A [,] B ) ) )
108 oveq1 
 |-  ( x = ( F ` A ) -> ( x [,] y ) = ( ( F ` A ) [,] y ) )
109 108 sseq1d 
 |-  ( x = ( F ` A ) -> ( ( x [,] y ) C_ ( F " ( A [,] B ) ) <-> ( ( F ` A ) [,] y ) C_ ( F " ( A [,] B ) ) ) )
110 oveq2 
 |-  ( y = ( F ` B ) -> ( ( F ` A ) [,] y ) = ( ( F ` A ) [,] ( F ` B ) ) )
111 110 sseq1d 
 |-  ( y = ( F ` B ) -> ( ( ( F ` A ) [,] y ) C_ ( F " ( A [,] B ) ) <-> ( ( F ` A ) [,] ( F ` B ) ) C_ ( F " ( A [,] B ) ) ) )
112 109 111 rspc2v 
 |-  ( ( ( F ` A ) e. ( F " ( A [,] B ) ) /\ ( F ` B ) e. ( F " ( A [,] B ) ) ) -> ( A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) -> ( ( F ` A ) [,] ( F ` B ) ) C_ ( F " ( A [,] B ) ) ) )
113 103 107 112 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( A. x e. ( F " ( A [,] B ) ) A. y e. ( F " ( A [,] B ) ) ( x [,] y ) C_ ( F " ( A [,] B ) ) -> ( ( F ` A ) [,] ( F ` B ) ) C_ ( F " ( A [,] B ) ) ) )
114 91 113 mpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( F ` A ) [,] ( F ` B ) ) C_ ( F " ( A [,] B ) ) )
115 ioossicc 
 |-  ( ( F ` A ) (,) ( F ` B ) ) C_ ( ( F ` A ) [,] ( F ` B ) )
116 115 sseli 
 |-  ( U e. ( ( F ` A ) (,) ( F ` B ) ) -> U e. ( ( F ` A ) [,] ( F ` B ) ) )
117 116 3ad2ant3 
 |-  ( ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) -> U e. ( ( F ` A ) [,] ( F ` B ) ) )
118 117 3ad2ant3 
 |-  ( ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) -> U e. ( ( F ` A ) [,] ( F ` B ) ) )
119 118 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U e. ( ( F ` A ) [,] ( F ` B ) ) )
120 114 119 sseldd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U e. ( F " ( A [,] B ) ) )
121 fvelima 
 |-  ( ( Fun F /\ U e. ( F " ( A [,] B ) ) ) -> E. x e. ( A [,] B ) ( F ` x ) = U )
122 6 120 121 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> E. x e. ( A [,] B ) ( F ` x ) = U )
123 simpl1 
 |-  ( ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) -> x e. RR* )
124 123 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) -> x e. RR* ) )
125 simprr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> ( F ` x ) = U )
126 24 103 sseldd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` A ) e. RR )
127 simp333 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U e. ( ( F ` A ) (,) ( F ` B ) ) )
128 126 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` A ) e. RR* )
129 24 107 sseldd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` B ) e. RR )
130 129 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` B ) e. RR* )
131 elioo2 
 |-  ( ( ( F ` A ) e. RR* /\ ( F ` B ) e. RR* ) -> ( U e. ( ( F ` A ) (,) ( F ` B ) ) <-> ( U e. RR /\ ( F ` A ) < U /\ U < ( F ` B ) ) ) )
132 128 130 131 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( U e. ( ( F ` A ) (,) ( F ` B ) ) <-> ( U e. RR /\ ( F ` A ) < U /\ U < ( F ` B ) ) ) )
133 127 132 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( U e. RR /\ ( F ` A ) < U /\ U < ( F ` B ) ) )
134 133 simp2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( F ` A ) < U )
135 126 134 gtned 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U =/= ( F ` A ) )
136 135 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> U =/= ( F ` A ) )
137 125 136 eqnetrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> ( F ` x ) =/= ( F ` A ) )
138 137 neneqd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> -. ( F ` x ) = ( F ` A ) )
139 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
140 138 139 nsyl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> -. x = A )
141 simp13 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U e. RR )
142 133 simp3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U < ( F ` B ) )
143 141 142 ltned 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> U =/= ( F ` B ) )
144 143 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> U =/= ( F ` B ) )
145 125 144 eqnetrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> ( F ` x ) =/= ( F ` B ) )
146 145 neneqd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> -. ( F ` x ) = ( F ` B ) )
147 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
148 146 147 nsyl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> -. x = B )
149 simprl3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> ( x = A \/ ( A < x /\ x < B ) \/ x = B ) )
150 140 148 149 ecase13d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) /\ ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) -> ( A < x /\ x < B ) )
151 150 ex 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) -> ( A < x /\ x < B ) ) )
152 124 151 jcad 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) -> ( x e. RR* /\ ( A < x /\ x < B ) ) ) )
153 3anass 
 |-  ( ( x e. RR* /\ A < x /\ x < B ) <-> ( x e. RR* /\ ( A < x /\ x < B ) ) )
154 152 153 syl6ibr 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) -> ( x e. RR* /\ A < x /\ x < B ) ) )
155 rexr 
 |-  ( A e. RR -> A e. RR* )
156 rexr 
 |-  ( B e. RR -> B e. RR* )
157 elicc3 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) ) )
158 155 156 157 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) ) )
159 158 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ U e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) ) )
160 159 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) ) )
161 160 anbi1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( x e. ( A [,] B ) /\ ( F ` x ) = U ) <-> ( ( x e. RR* /\ A <_ B /\ ( x = A \/ ( A < x /\ x < B ) \/ x = B ) ) /\ ( F ` x ) = U ) ) )
162 elioo1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A (,) B ) <-> ( x e. RR* /\ A < x /\ x < B ) ) )
163 155 156 162 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A (,) B ) <-> ( x e. RR* /\ A < x /\ x < B ) ) )
164 163 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ U e. RR ) -> ( x e. ( A (,) B ) <-> ( x e. RR* /\ A < x /\ x < B ) ) )
165 164 3ad2ant1 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( x e. ( A (,) B ) <-> ( x e. RR* /\ A < x /\ x < B ) ) )
166 154 161 165 3imtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( x e. ( A [,] B ) /\ ( F ` x ) = U ) -> x e. ( A (,) B ) ) )
167 simpr 
 |-  ( ( x e. ( A [,] B ) /\ ( F ` x ) = U ) -> ( F ` x ) = U )
168 167 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( x e. ( A [,] B ) /\ ( F ` x ) = U ) -> ( F ` x ) = U ) )
169 166 168 jcad 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( ( x e. ( A [,] B ) /\ ( F ` x ) = U ) -> ( x e. ( A (,) B ) /\ ( F ` x ) = U ) ) )
170 169 reximdv2 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> ( E. x e. ( A [,] B ) ( F ` x ) = U -> E. x e. ( A (,) B ) ( F ` x ) = U ) )
171 122 170 mpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> E. x e. ( A (,) B ) ( F ` x ) = U )