Metamath Proof Explorer

Theorem evthicc2

Description: Combine ivthicc with evthicc to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses evthicc.1 
|- ( ph -> A e. RR )
evthicc.2 
|- ( ph -> B e. RR )
evthicc.3 
|- ( ph -> A <_ B )
evthicc.4 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
Assertion evthicc2 
|- ( ph -> E. x e. RR E. y e. RR ran F = ( x [,] y ) )

Proof

Step Hyp Ref Expression
1 evthicc.1 
 |-  ( ph -> A e. RR )
2 evthicc.2 
 |-  ( ph -> B e. RR )
3 evthicc.3 
 |-  ( ph -> A <_ B )
4 evthicc.4 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
5 1 2 3 4 evthicc 
 |-  ( ph -> ( E. a e. ( A [,] B ) A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ E. b e. ( A [,] B ) A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) )
6 reeanv 
 |-  ( E. a e. ( A [,] B ) E. b e. ( A [,] B ) ( A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) <-> ( E. a e. ( A [,] B ) A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ E. b e. ( A [,] B ) A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) )
7 5 6 sylibr 
 |-  ( ph -> E. a e. ( A [,] B ) E. b e. ( A [,] B ) ( A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) )
8 r19.26 
 |-  ( A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) <-> ( A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) )
9 4 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> F e. ( ( A [,] B ) -cn-> RR ) )
10 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
11 9 10 syl 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> F : ( A [,] B ) --> RR )
12 simprr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> b e. ( A [,] B ) )
13 11 12 ffvelrnd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` b ) e. RR )
14 13 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> ( F ` b ) e. RR )
15 simprl 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> a e. ( A [,] B ) )
16 11 15 ffvelrnd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( F ` a ) e. RR )
17 16 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> ( F ` a ) e. RR )
18 11 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> F : ( A [,] B ) --> RR )
19 18 ffnd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> F Fn ( A [,] B ) )
20 16 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( F ` a ) e. RR )
21 elicc2 
 |-  ( ( ( F ` b ) e. RR /\ ( F ` a ) e. RR ) -> ( ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) <-> ( ( F ` z ) e. RR /\ ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) )
22 13 20 21 syl2an2r 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) <-> ( ( F ` z ) e. RR /\ ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) )
23 3anass 
 |-  ( ( ( F ` z ) e. RR /\ ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) <-> ( ( F ` z ) e. RR /\ ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) )
24 22 23 bitrdi 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) <-> ( ( F ` z ) e. RR /\ ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) ) )
25 ancom 
 |-  ( ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) <-> ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) )
26 11 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. RR )
27 26 biantrurd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) <-> ( ( F ` z ) e. RR /\ ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) ) )
28 25 27 syl5bb 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) <-> ( ( F ` z ) e. RR /\ ( ( F ` b ) <_ ( F ` z ) /\ ( F ` z ) <_ ( F ` a ) ) ) ) )
29 24 28 bitr4d 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ z e. ( A [,] B ) ) -> ( ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) <-> ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) )
30 29 ralbidva 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( A. z e. ( A [,] B ) ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) <-> A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) )
31 30 biimpar 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> A. z e. ( A [,] B ) ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) )
32 ffnfv 
 |-  ( F : ( A [,] B ) --> ( ( F ` b ) [,] ( F ` a ) ) <-> ( F Fn ( A [,] B ) /\ A. z e. ( A [,] B ) ( F ` z ) e. ( ( F ` b ) [,] ( F ` a ) ) ) )
33 19 31 32 sylanbrc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> F : ( A [,] B ) --> ( ( F ` b ) [,] ( F ` a ) ) )
34 33 frnd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> ran F C_ ( ( F ` b ) [,] ( F ` a ) ) )
35 1 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> A e. RR )
36 2 adantr 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> B e. RR )
37 ssidd 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( A [,] B ) C_ ( A [,] B ) )
38 ax-resscn 
 |-  RR C_ CC
39 ssid 
 |-  CC C_ CC
40 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
41 38 39 40 mp2an 
 |-  ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
42 41 9 sseldi 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> F e. ( ( A [,] B ) -cn-> CC ) )
43 11 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
44 35 36 12 15 37 42 43 ivthicc 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( F ` b ) [,] ( F ` a ) ) C_ ran F )
45 44 adantr 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> ( ( F ` b ) [,] ( F ` a ) ) C_ ran F )
46 34 45 eqssd 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> ran F = ( ( F ` b ) [,] ( F ` a ) ) )
47 rspceov 
 |-  ( ( ( F ` b ) e. RR /\ ( F ` a ) e. RR /\ ran F = ( ( F ` b ) [,] ( F ` a ) ) ) -> E. x e. RR E. y e. RR ran F = ( x [,] y ) )
48 14 17 46 47 syl3anc 
 |-  ( ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) /\ A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) ) -> E. x e. RR E. y e. RR ran F = ( x [,] y ) )
49 48 ex 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( A. z e. ( A [,] B ) ( ( F ` z ) <_ ( F ` a ) /\ ( F ` b ) <_ ( F ` z ) ) -> E. x e. RR E. y e. RR ran F = ( x [,] y ) ) )
50 8 49 syl5bir 
 |-  ( ( ph /\ ( a e. ( A [,] B ) /\ b e. ( A [,] B ) ) ) -> ( ( A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) -> E. x e. RR E. y e. RR ran F = ( x [,] y ) ) )
51 50 rexlimdvva 
 |-  ( ph -> ( E. a e. ( A [,] B ) E. b e. ( A [,] B ) ( A. z e. ( A [,] B ) ( F ` z ) <_ ( F ` a ) /\ A. z e. ( A [,] B ) ( F ` b ) <_ ( F ` z ) ) -> E. x e. RR E. y e. RR ran F = ( x [,] y ) ) )
52 7 51 mpd 
 |-  ( ph -> E. x e. RR E. y e. RR ran F = ( x [,] y ) )