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

Proof

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