Metamath Proof Explorer

Theorem iocopnst

Description: A half-open interval ending at B is open in the closed interval from A to B . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis iocopnst.1 ⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
Assertion iocopnst ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 iocopnst.1 ⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
2 iooretop ⊢ ( 𝐶 (,) ( 𝐵 + 1 ) ) ∈ ( topGen ‘ ran (,) )
3 simp1 ⊢ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 ∈ ℝ )
4 3 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 ∈ ℝ ) )
5 simp2 ⊢ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐶 < 𝑣 )
6 5 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐶 < 𝑣 ) )
7 ltp1 ⊢ ( 𝐵 ∈ ℝ → 𝐵 < ( 𝐵 + 1 ) )
8 7 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → 𝐵 < ( 𝐵 + 1 ) )
9 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
10 lelttr ⊢ ( ( 𝑣 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 𝑣 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 𝑣 < ( 𝐵 + 1 ) ) )
11 10 3expa ⊢ ( ( ( 𝑣 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 𝑣 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 𝑣 < ( 𝐵 + 1 ) ) )
12 11 ancom1s ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝑣 ∈ ℝ ) ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 𝑣 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 𝑣 < ( 𝐵 + 1 ) ) )
13 12 ancomsd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝑣 ∈ ℝ ) ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 𝐵 < ( 𝐵 + 1 ) ∧ 𝑣 ≤ 𝐵 ) → 𝑣 < ( 𝐵 + 1 ) ) )
14 9 13 mpidan ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( ( 𝐵 < ( 𝐵 + 1 ) ∧ 𝑣 ≤ 𝐵 ) → 𝑣 < ( 𝐵 + 1 ) ) )
15 8 14 mpand ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝑣 ≤ 𝐵 → 𝑣 < ( 𝐵 + 1 ) ) )
16 15 impr ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑣 ∈ ℝ ∧ 𝑣 ≤ 𝐵 ) ) → 𝑣 < ( 𝐵 + 1 ) )
17 16 3adantr2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → 𝑣 < ( 𝐵 + 1 ) )
18 17 ex ⊢ ( 𝐵 ∈ ℝ → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 < ( 𝐵 + 1 ) ) )
19 18 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 < ( 𝐵 + 1 ) ) )
20 4 6 19 3jcad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ) )
21 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
22 elico2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
23 21 22 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
24 23 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) )
25 lelttr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝑣 ) → 𝐴 < 𝑣 ) )
26 ltle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝐴 < 𝑣 → 𝐴 ≤ 𝑣 ) )
27 26 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝐴 < 𝑣 → 𝐴 ≤ 𝑣 ) )
28 25 27 syld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝑣 ) → 𝐴 ≤ 𝑣 ) )
29 28 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑣 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝑣 ) → 𝐴 ≤ 𝑣 ) )
30 29 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑣 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝑣 ) ) → 𝐴 ≤ 𝑣 )
31 30 an4s ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 ≤ 𝐶 ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ) ) → 𝐴 ≤ 𝑣 )
32 31 3adantr3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 ≤ 𝐶 ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → 𝐴 ≤ 𝑣 )
33 32 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 ≤ 𝐶 ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐴 ≤ 𝑣 ) )
34 33 anasss ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐴 ≤ 𝑣 ) )
35 34 3adantr3 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐴 ≤ 𝑣 ) )
36 35 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐴 ≤ 𝑣 ) )
37 24 36 syldan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝐴 ≤ 𝑣 ) )
38 simp3 ⊢ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 ≤ 𝐵 )
39 38 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → 𝑣 ≤ 𝐵 ) )
40 4 37 39 3jcad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) )
41 20 40 jcad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) ) )
42 simpl1 ⊢ ( ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → 𝑣 ∈ ℝ )
43 simpl2 ⊢ ( ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → 𝐶 < 𝑣 )
44 simpr3 ⊢ ( ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → 𝑣 ≤ 𝐵 )
45 42 43 44 3jca ⊢ ( ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) → ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) )
46 41 45 impbid1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) ↔ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) ) )
47 24 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ )
48 47 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ* )
49 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ℝ )
50 elioc2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝑣 ∈ ( 𝐶 (,] 𝐵 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) )
51 48 49 50 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐶 (,] 𝐵 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) )
52 elin ⊢ ( 𝑣 ∈ ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝑣 ∈ ( 𝐶 (,) ( 𝐵 + 1 ) ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) )
53 9 rexrd ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ* )
54 53 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐵 + 1 ) ∈ ℝ* )
55 elioo2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ ( 𝐵 + 1 ) ∈ ℝ* ) → ( 𝑣 ∈ ( 𝐶 (,) ( 𝐵 + 1 ) ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ) )
56 48 54 55 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐶 (,) ( 𝐵 + 1 ) ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ) )
57 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) )
58 57 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) )
59 56 58 anbi12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑣 ∈ ( 𝐶 (,) ( 𝐵 + 1 ) ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) ) )
60 52 59 bitrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( 𝑣 ∈ ℝ ∧ 𝐶 < 𝑣 ∧ 𝑣 < ( 𝐵 + 1 ) ) ∧ ( 𝑣 ∈ ℝ ∧ 𝐴 ≤ 𝑣 ∧ 𝑣 ≤ 𝐵 ) ) ) )
61 46 51 60 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( 𝐶 (,] 𝐵 ) ↔ 𝑣 ∈ ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) ) )
62 61 eqrdv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐶 (,] 𝐵 ) = ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
63 ineq1 ⊢ ( 𝑣 = ( 𝐶 (,) ( 𝐵 + 1 ) ) → ( 𝑣 ∩ ( 𝐴 [,] 𝐵 ) ) = ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
64 63 rspceeqv ⊢ ( ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∈ ( topGen ‘ ran (,) ) ∧ ( 𝐶 (,] 𝐵 ) = ( ( 𝐶 (,) ( 𝐵 + 1 ) ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑣 ∈ ( topGen ‘ ran (,) ) ( 𝐶 (,] 𝐵 ) = ( 𝑣 ∩ ( 𝐴 [,] 𝐵 ) ) )
65 2 62 64 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ∃ 𝑣 ∈ ( topGen ‘ ran (,) ) ( 𝐶 (,] 𝐵 ) = ( 𝑣 ∩ ( 𝐴 [,] 𝐵 ) ) )
66 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
67 ovex ⊢ ( 𝐴 [,] 𝐵 ) ∈ V
68 elrest ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ∈ V ) → ( ( 𝐶 (,] 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ↔ ∃ 𝑣 ∈ ( topGen ‘ ran (,) ) ( 𝐶 (,] 𝐵 ) = ( 𝑣 ∩ ( 𝐴 [,] 𝐵 ) ) ) )
69 66 67 68 mp2an ⊢ ( ( 𝐶 (,] 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ↔ ∃ 𝑣 ∈ ( topGen ‘ ran (,) ) ( 𝐶 (,] 𝐵 ) = ( 𝑣 ∩ ( 𝐴 [,] 𝐵 ) ) )
70 65 69 sylibr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐶 (,] 𝐵 ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
71 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
72 71 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
73 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
74 73 1 resubmet ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
75 72 74 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
76 70 75 eleqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 )
77 76 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 ) )