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 ⊢ ( 𝜑 → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 )