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
|
syl5bb |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑣 ∈ ( ( 𝐶 (,) ( 𝐵 + 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 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝐶 (,] 𝐵 ) ∈ 𝐽 ) ) |