Metamath Proof Explorer

Theorem icoopnst

Description: A half-open interval starting at A 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 icoopnst.1 
|- J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )
Assertion icoopnst 
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A (,] B ) -> ( A [,) C ) e. J ) )

Proof

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