Metamath Proof Explorer

Theorem icoopn

Description: A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses icoopn.a 
|- ( ph -> A e. RR )
icoopn.c 
|- ( ph -> C e. RR* )
icoopn.b 
|- ( ph -> B e. RR* )
icoopn.k 
|- K = ( topGen ` ran (,) )
icoopn.j 
|- J = ( K |`t ( A [,) B ) )
icoopn.cleb 
|- ( ph -> C <_ B )
Assertion icoopn 
|- ( ph -> ( A [,) C ) e. J )

Proof

Step Hyp Ref Expression
1 icoopn.a 
 |-  ( ph -> A e. RR )
2 icoopn.c 
 |-  ( ph -> C e. RR* )
3 icoopn.b 
 |-  ( ph -> B e. RR* )
4 icoopn.k 
 |-  K = ( topGen ` ran (,) )
5 icoopn.j 
 |-  J = ( K |`t ( A [,) B ) )
6 icoopn.cleb 
 |-  ( ph -> C <_ B )
7 retop 
 |-  ( topGen ` ran (,) ) e. Top
8 4 7 eqeltri 
 |-  K e. Top
9 8 a1i 
 |-  ( ph -> K e. Top )
10 ovexd 
 |-  ( ph -> ( A [,) B ) e. _V )
11 iooretop 
 |-  ( -oo (,) C ) e. ( topGen ` ran (,) )
12 11 4 eleqtrri 
 |-  ( -oo (,) C ) e. K
13 12 a1i 
 |-  ( ph -> ( -oo (,) C ) e. K )
14 elrestr 
 |-  ( ( K e. Top /\ ( A [,) B ) e. _V /\ ( -oo (,) C ) e. K ) -> ( ( -oo (,) C ) i^i ( A [,) B ) ) e. ( K |`t ( A [,) B ) ) )
15 9 10 13 14 syl3anc 
 |-  ( ph -> ( ( -oo (,) C ) i^i ( A [,) B ) ) e. ( K |`t ( A [,) B ) ) )
16 1 rexrd 
 |-  ( ph -> A e. RR* )
17 16 adantr 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> A e. RR* )
18 2 adantr 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> C e. RR* )
19 elinel1 
 |-  ( x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) -> x e. ( -oo (,) C ) )
20 elioore 
 |-  ( x e. ( -oo (,) C ) -> x e. RR )
21 19 20 syl 
 |-  ( x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) -> x e. RR )
22 21 rexrd 
 |-  ( x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) -> x e. RR* )
23 22 adantl 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> x e. RR* )
24 3 adantr 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> B e. RR* )
25 elinel2 
 |-  ( x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) -> x e. ( A [,) B ) )
26 25 adantl 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> x e. ( A [,) B ) )
27 icogelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,) B ) ) -> A <_ x )
28 17 24 26 27 syl3anc 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> A <_ x )
29 mnfxr 
 |-  -oo e. RR*
30 29 a1i 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> -oo e. RR* )
31 19 adantl 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> x e. ( -oo (,) C ) )
32 iooltub 
 |-  ( ( -oo e. RR* /\ C e. RR* /\ x e. ( -oo (,) C ) ) -> x < C )
33 30 18 31 32 syl3anc 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> x < C )
34 17 18 23 28 33 elicod 
 |-  ( ( ph /\ x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) ) -> x e. ( A [,) C ) )
35 29 a1i 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> -oo e. RR* )
36 2 adantr 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> C e. RR* )
37 icossre 
 |-  ( ( A e. RR /\ C e. RR* ) -> ( A [,) C ) C_ RR )
38 1 2 37 syl2anc 
 |-  ( ph -> ( A [,) C ) C_ RR )
39 38 sselda 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. RR )
40 39 mnfltd 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> -oo < x )
41 16 adantr 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> A e. RR* )
42 simpr 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. ( A [,) C ) )
43 icoltub 
 |-  ( ( A e. RR* /\ C e. RR* /\ x e. ( A [,) C ) ) -> x < C )
44 41 36 42 43 syl3anc 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x < C )
45 35 36 39 40 44 eliood 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. ( -oo (,) C ) )
46 3 adantr 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> B e. RR* )
47 39 rexrd 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. RR* )
48 icogelb 
 |-  ( ( A e. RR* /\ C e. RR* /\ x e. ( A [,) C ) ) -> A <_ x )
49 41 36 42 48 syl3anc 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> A <_ x )
50 6 adantr 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> C <_ B )
51 47 36 46 44 50 xrltletrd 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x < B )
52 41 46 47 49 51 elicod 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. ( A [,) B ) )
53 45 52 elind 
 |-  ( ( ph /\ x e. ( A [,) C ) ) -> x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) )
54 34 53 impbida 
 |-  ( ph -> ( x e. ( ( -oo (,) C ) i^i ( A [,) B ) ) <-> x e. ( A [,) C ) ) )
55 54 eqrdv 
 |-  ( ph -> ( ( -oo (,) C ) i^i ( A [,) B ) ) = ( A [,) C ) )
56 5 eqcomi 
 |-  ( K |`t ( A [,) B ) ) = J
57 56 a1i 
 |-  ( ph -> ( K |`t ( A [,) B ) ) = J )
58 15 55 57 3eltr3d 
 |-  ( ph -> ( A [,) C ) e. J )