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 bitrid 
 |-  ( ( ( 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 ) )