Metamath Proof Explorer

Theorem iocopn

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

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

Proof

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