Metamath Proof Explorer

Theorem icoopnst

Description: A half-open interval starting at A 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 icoopnst.1 ⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 𝐴 [,] 𝐵 ) × ( 𝐴 [,] 𝐵 ) ) ) )
Assertion icoopnst ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 (,] 𝐵 ) → ( 𝐴 [,) 𝐶 ) ∈ 𝐽 ) )

Proof

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