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 ( 𝜑𝐴 ∈ ℝ )
icoopn.c ( 𝜑𝐶 ∈ ℝ* )
icoopn.b ( 𝜑𝐵 ∈ ℝ* )
icoopn.k 𝐾 = ( topGen ‘ ran (,) )
icoopn.j 𝐽 = ( 𝐾t ( 𝐴 [,) 𝐵 ) )
icoopn.cleb ( 𝜑𝐶𝐵 )
Assertion icoopn ( 𝜑 → ( 𝐴 [,) 𝐶 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 icoopn.a ( 𝜑𝐴 ∈ ℝ )
2 icoopn.c ( 𝜑𝐶 ∈ ℝ* )
3 icoopn.b ( 𝜑𝐵 ∈ ℝ* )
4 icoopn.k 𝐾 = ( topGen ‘ ran (,) )
5 icoopn.j 𝐽 = ( 𝐾t ( 𝐴 [,) 𝐵 ) )
6 icoopn.cleb ( 𝜑𝐶𝐵 )
7 retop ( topGen ‘ ran (,) ) ∈ Top
8 4 7 eqeltri 𝐾 ∈ Top
9 8 a1i ( 𝜑𝐾 ∈ Top )
10 ovexd ( 𝜑 → ( 𝐴 [,) 𝐵 ) ∈ V )
11 iooretop ( -∞ (,) 𝐶 ) ∈ ( topGen ‘ ran (,) )
12 11 4 eleqtrri ( -∞ (,) 𝐶 ) ∈ 𝐾
13 12 a1i ( 𝜑 → ( -∞ (,) 𝐶 ) ∈ 𝐾 )
14 elrestr ( ( 𝐾 ∈ Top ∧ ( 𝐴 [,) 𝐵 ) ∈ V ∧ ( -∞ (,) 𝐶 ) ∈ 𝐾 ) → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ∈ ( 𝐾t ( 𝐴 [,) 𝐵 ) ) )
15 9 10 13 14 syl3anc ( 𝜑 → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ∈ ( 𝐾t ( 𝐴 [,) 𝐵 ) ) )
16 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
17 16 adantr ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐴 ∈ ℝ* )
18 2 adantr ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐶 ∈ ℝ* )
19 elinel1 ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
20 elioore ( 𝑥 ∈ ( -∞ (,) 𝐶 ) → 𝑥 ∈ ℝ )
21 19 20 syl ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ )
22 21 rexrd ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ* )
23 22 adantl ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ℝ* )
24 3 adantr ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐵 ∈ ℝ* )
25 elinel2 ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
26 25 adantl ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
27 icogelb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴𝑥 )
28 17 24 26 27 syl3anc ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝐴𝑥 )
29 mnfxr -∞ ∈ ℝ*
30 29 a1i ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → -∞ ∈ ℝ* )
31 19 adantl ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
32 iooltub ( ( -∞ ∈ ℝ*𝐶 ∈ ℝ*𝑥 ∈ ( -∞ (,) 𝐶 ) ) → 𝑥 < 𝐶 )
33 30 18 31 32 syl3anc ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 < 𝐶 )
34 17 18 23 28 33 elicod ( ( 𝜑𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐶 ) )
35 29 a1i ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → -∞ ∈ ℝ* )
36 2 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐶 ∈ ℝ* )
37 icossre ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 [,) 𝐶 ) ⊆ ℝ )
38 1 2 37 syl2anc ( 𝜑 → ( 𝐴 [,) 𝐶 ) ⊆ ℝ )
39 38 sselda ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ℝ )
40 39 mnfltd ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → -∞ < 𝑥 )
41 16 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴 ∈ ℝ* )
42 simpr ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐶 ) )
43 icoltub ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐶 )
44 41 36 42 43 syl3anc ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐶 )
45 35 36 39 40 44 eliood ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( -∞ (,) 𝐶 ) )
46 3 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐵 ∈ ℝ* )
47 39 rexrd ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ℝ* )
48 icogelb ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴𝑥 )
49 41 36 42 48 syl3anc ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐴𝑥 )
50 6 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝐶𝐵 )
51 47 36 46 44 50 xrltletrd ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 < 𝐵 )
52 41 46 47 49 51 elicod ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
53 45 52 elind ( ( 𝜑𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) → 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) )
54 34 53 impbida ( 𝜑 → ( 𝑥 ∈ ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) ↔ 𝑥 ∈ ( 𝐴 [,) 𝐶 ) ) )
55 54 eqrdv ( 𝜑 → ( ( -∞ (,) 𝐶 ) ∩ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) 𝐶 ) )
56 5 eqcomi ( 𝐾t ( 𝐴 [,) 𝐵 ) ) = 𝐽
57 56 a1i ( 𝜑 → ( 𝐾t ( 𝐴 [,) 𝐵 ) ) = 𝐽 )
58 15 55 57 3eltr3d ( 𝜑 → ( 𝐴 [,) 𝐶 ) ∈ 𝐽 )