Metamath Proof Explorer


Theorem iocopnst

Description: A half-open interval ending at B is open in the closed interval from A to B . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis iocopnst.1
|- J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )
Assertion iocopnst
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) -> ( C (,] B ) e. J ) )

Proof

Step Hyp Ref Expression
1 iocopnst.1
 |-  J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )
2 iooretop
 |-  ( C (,) ( B + 1 ) ) e. ( topGen ` ran (,) )
3 simp1
 |-  ( ( v e. RR /\ C < v /\ v <_ B ) -> v e. RR )
4 3 a1i
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v e. RR ) )
5 simp2
 |-  ( ( v e. RR /\ C < v /\ v <_ B ) -> C < v )
6 5 a1i
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> C < v ) )
7 ltp1
 |-  ( B e. RR -> B < ( B + 1 ) )
8 7 adantr
 |-  ( ( B e. RR /\ v e. RR ) -> B < ( B + 1 ) )
9 peano2re
 |-  ( B e. RR -> ( B + 1 ) e. RR )
10 lelttr
 |-  ( ( v e. RR /\ B e. RR /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) )
11 10 3expa
 |-  ( ( ( v e. RR /\ B e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) )
12 11 ancom1s
 |-  ( ( ( B e. RR /\ v e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) )
13 12 ancomsd
 |-  ( ( ( B e. RR /\ v e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( B < ( B + 1 ) /\ v <_ B ) -> v < ( B + 1 ) ) )
14 9 13 mpidan
 |-  ( ( B e. RR /\ v e. RR ) -> ( ( B < ( B + 1 ) /\ v <_ B ) -> v < ( B + 1 ) ) )
15 8 14 mpand
 |-  ( ( B e. RR /\ v e. RR ) -> ( v <_ B -> v < ( B + 1 ) ) )
16 15 impr
 |-  ( ( B e. RR /\ ( v e. RR /\ v <_ B ) ) -> v < ( B + 1 ) )
17 16 3adantr2
 |-  ( ( B e. RR /\ ( v e. RR /\ C < v /\ v <_ B ) ) -> v < ( B + 1 ) )
18 17 ex
 |-  ( B e. RR -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v < ( B + 1 ) ) )
19 18 ad2antlr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v < ( B + 1 ) ) )
20 4 6 19 3jcad
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) )
21 rexr
 |-  ( B e. RR -> B e. RR* )
22 elico2
 |-  ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
23 21 22 sylan2
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
24 23 biimpa
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C e. RR /\ A <_ C /\ C < B ) )
25 lelttr
 |-  ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A < v ) )
26 ltle
 |-  ( ( A e. RR /\ v e. RR ) -> ( A < v -> A <_ v ) )
27 26 3adant2
 |-  ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( A < v -> A <_ v ) )
28 25 27 syld
 |-  ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A <_ v ) )
29 28 3expa
 |-  ( ( ( A e. RR /\ C e. RR ) /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A <_ v ) )
30 29 imp
 |-  ( ( ( ( A e. RR /\ C e. RR ) /\ v e. RR ) /\ ( A <_ C /\ C < v ) ) -> A <_ v )
31 30 an4s
 |-  ( ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) /\ ( v e. RR /\ C < v ) ) -> A <_ v )
32 31 3adantr3
 |-  ( ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) /\ ( v e. RR /\ C < v /\ v <_ B ) ) -> A <_ v )
33 32 ex
 |-  ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) )
34 33 anasss
 |-  ( ( A e. RR /\ ( C e. RR /\ A <_ C ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) )
35 34 3adantr3
 |-  ( ( A e. RR /\ ( C e. RR /\ A <_ C /\ C < B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) )
36 35 adantlr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ A <_ C /\ C < B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) )
37 24 36 syldan
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) )
38 simp3
 |-  ( ( v e. RR /\ C < v /\ v <_ B ) -> v <_ B )
39 38 a1i
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v <_ B ) )
40 4 37 39 3jcad
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( v e. RR /\ A <_ v /\ v <_ B ) ) )
41 20 40 jcad
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) )
42 simpl1
 |-  ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> v e. RR )
43 simpl2
 |-  ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> C < v )
44 simpr3
 |-  ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> v <_ B )
45 42 43 44 3jca
 |-  ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> ( v e. RR /\ C < v /\ v <_ B ) )
46 41 45 impbid1
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) )
47 24 simp1d
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> C e. RR )
48 47 rexrd
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> C e. RR* )
49 simplr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> B e. RR )
50 elioc2
 |-  ( ( C e. RR* /\ B e. RR ) -> ( v e. ( C (,] B ) <-> ( v e. RR /\ C < v /\ v <_ B ) ) )
51 48 49 50 syl2anc
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,] B ) <-> ( v e. RR /\ C < v /\ v <_ B ) ) )
52 elin
 |-  ( v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) <-> ( v e. ( C (,) ( B + 1 ) ) /\ v e. ( A [,] B ) ) )
53 9 rexrd
 |-  ( B e. RR -> ( B + 1 ) e. RR* )
54 53 ad2antlr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( B + 1 ) e. RR* )
55 elioo2
 |-  ( ( C e. RR* /\ ( B + 1 ) e. RR* ) -> ( v e. ( C (,) ( B + 1 ) ) <-> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) )
56 48 54 55 syl2anc
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,) ( B + 1 ) ) <-> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) )
57 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( v e. ( A [,] B ) <-> ( v e. RR /\ A <_ v /\ v <_ B ) ) )
58 57 adantr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( A [,] B ) <-> ( v e. RR /\ A <_ v /\ v <_ B ) ) )
59 56 58 anbi12d
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. ( C (,) ( B + 1 ) ) /\ v e. ( A [,] B ) ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) )
60 52 59 syl5bb
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) )
61 46 51 60 3bitr4d
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,] B ) <-> v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) )
62 61 eqrdv
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) )
63 ineq1
 |-  ( v = ( C (,) ( B + 1 ) ) -> ( v i^i ( A [,] B ) ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) )
64 63 rspceeqv
 |-  ( ( ( C (,) ( B + 1 ) ) e. ( topGen ` ran (,) ) /\ ( C (,] B ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) -> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) )
65 2 62 64 sylancr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) )
66 retop
 |-  ( topGen ` ran (,) ) e. Top
67 ovex
 |-  ( A [,] B ) e. _V
68 elrest
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) <-> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) ) )
69 66 67 68 mp2an
 |-  ( ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) <-> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) )
70 65 69 sylibr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
71 iccssre
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
72 71 adantr
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( A [,] B ) C_ RR )
73 eqid
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
74 73 1 resubmet
 |-  ( ( A [,] B ) C_ RR -> J = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
75 72 74 syl
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> J = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
76 70 75 eleqtrrd
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) e. J )
77 76 ex
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) -> ( C (,] B ) e. J ) )