Step |
Hyp |
Ref |
Expression |
1 |
|
iocopnst.1 |
|- J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) ) |
2 |
|
iooretop |
|- ( C (,) ( B + 1 ) ) e. ( topGen ` ran (,) ) |
3 |
|
simp1 |
|- ( ( v e. RR /\ C < v /\ v <_ B ) -> v e. RR ) |
4 |
3
|
a1i |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v e. RR ) ) |
5 |
|
simp2 |
|- ( ( v e. RR /\ C < v /\ v <_ B ) -> C < v ) |
6 |
5
|
a1i |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> C < v ) ) |
7 |
|
ltp1 |
|- ( B e. RR -> B < ( B + 1 ) ) |
8 |
7
|
adantr |
|- ( ( B e. RR /\ v e. RR ) -> B < ( B + 1 ) ) |
9 |
|
peano2re |
|- ( B e. RR -> ( B + 1 ) e. RR ) |
10 |
|
lelttr |
|- ( ( v e. RR /\ B e. RR /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) ) |
11 |
10
|
3expa |
|- ( ( ( v e. RR /\ B e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) ) |
12 |
11
|
ancom1s |
|- ( ( ( B e. RR /\ v e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( v <_ B /\ B < ( B + 1 ) ) -> v < ( B + 1 ) ) ) |
13 |
12
|
ancomsd |
|- ( ( ( B e. RR /\ v e. RR ) /\ ( B + 1 ) e. RR ) -> ( ( B < ( B + 1 ) /\ v <_ B ) -> v < ( B + 1 ) ) ) |
14 |
9 13
|
mpidan |
|- ( ( B e. RR /\ v e. RR ) -> ( ( B < ( B + 1 ) /\ v <_ B ) -> v < ( B + 1 ) ) ) |
15 |
8 14
|
mpand |
|- ( ( B e. RR /\ v e. RR ) -> ( v <_ B -> v < ( B + 1 ) ) ) |
16 |
15
|
impr |
|- ( ( B e. RR /\ ( v e. RR /\ v <_ B ) ) -> v < ( B + 1 ) ) |
17 |
16
|
3adantr2 |
|- ( ( B e. RR /\ ( v e. RR /\ C < v /\ v <_ B ) ) -> v < ( B + 1 ) ) |
18 |
17
|
ex |
|- ( B e. RR -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v < ( B + 1 ) ) ) |
19 |
18
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v < ( B + 1 ) ) ) |
20 |
4 6 19
|
3jcad |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) ) |
21 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
22 |
|
elico2 |
|- ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) ) |
23 |
21 22
|
sylan2 |
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) ) |
24 |
23
|
biimpa |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C e. RR /\ A <_ C /\ C < B ) ) |
25 |
|
lelttr |
|- ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A < v ) ) |
26 |
|
ltle |
|- ( ( A e. RR /\ v e. RR ) -> ( A < v -> A <_ v ) ) |
27 |
26
|
3adant2 |
|- ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( A < v -> A <_ v ) ) |
28 |
25 27
|
syld |
|- ( ( A e. RR /\ C e. RR /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A <_ v ) ) |
29 |
28
|
3expa |
|- ( ( ( A e. RR /\ C e. RR ) /\ v e. RR ) -> ( ( A <_ C /\ C < v ) -> A <_ v ) ) |
30 |
29
|
imp |
|- ( ( ( ( A e. RR /\ C e. RR ) /\ v e. RR ) /\ ( A <_ C /\ C < v ) ) -> A <_ v ) |
31 |
30
|
an4s |
|- ( ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) /\ ( v e. RR /\ C < v ) ) -> A <_ v ) |
32 |
31
|
3adantr3 |
|- ( ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) /\ ( v e. RR /\ C < v /\ v <_ B ) ) -> A <_ v ) |
33 |
32
|
ex |
|- ( ( ( A e. RR /\ C e. RR ) /\ A <_ C ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) ) |
34 |
33
|
anasss |
|- ( ( A e. RR /\ ( C e. RR /\ A <_ C ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) ) |
35 |
34
|
3adantr3 |
|- ( ( A e. RR /\ ( C e. RR /\ A <_ C /\ C < B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) ) |
36 |
35
|
adantlr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ A <_ C /\ C < B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) ) |
37 |
24 36
|
syldan |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> A <_ v ) ) |
38 |
|
simp3 |
|- ( ( v e. RR /\ C < v /\ v <_ B ) -> v <_ B ) |
39 |
38
|
a1i |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> v <_ B ) ) |
40 |
4 37 39
|
3jcad |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( v e. RR /\ A <_ v /\ v <_ B ) ) ) |
41 |
20 40
|
jcad |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) -> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) ) |
42 |
|
simpl1 |
|- ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> v e. RR ) |
43 |
|
simpl2 |
|- ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> C < v ) |
44 |
|
simpr3 |
|- ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> v <_ B ) |
45 |
42 43 44
|
3jca |
|- ( ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) -> ( v e. RR /\ C < v /\ v <_ B ) ) |
46 |
41 45
|
impbid1 |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. RR /\ C < v /\ v <_ B ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) ) |
47 |
24
|
simp1d |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> C e. RR ) |
48 |
47
|
rexrd |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> C e. RR* ) |
49 |
|
simplr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> B e. RR ) |
50 |
|
elioc2 |
|- ( ( C e. RR* /\ B e. RR ) -> ( v e. ( C (,] B ) <-> ( v e. RR /\ C < v /\ v <_ B ) ) ) |
51 |
48 49 50
|
syl2anc |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,] B ) <-> ( v e. RR /\ C < v /\ v <_ B ) ) ) |
52 |
|
elin |
|- ( v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) <-> ( v e. ( C (,) ( B + 1 ) ) /\ v e. ( A [,] B ) ) ) |
53 |
9
|
rexrd |
|- ( B e. RR -> ( B + 1 ) e. RR* ) |
54 |
53
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( B + 1 ) e. RR* ) |
55 |
|
elioo2 |
|- ( ( C e. RR* /\ ( B + 1 ) e. RR* ) -> ( v e. ( C (,) ( B + 1 ) ) <-> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) ) |
56 |
48 54 55
|
syl2anc |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,) ( B + 1 ) ) <-> ( v e. RR /\ C < v /\ v < ( B + 1 ) ) ) ) |
57 |
|
elicc2 |
|- ( ( A e. RR /\ B e. RR ) -> ( v e. ( A [,] B ) <-> ( v e. RR /\ A <_ v /\ v <_ B ) ) ) |
58 |
57
|
adantr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( A [,] B ) <-> ( v e. RR /\ A <_ v /\ v <_ B ) ) ) |
59 |
56 58
|
anbi12d |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( ( v e. ( C (,) ( B + 1 ) ) /\ v e. ( A [,] B ) ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) ) |
60 |
52 59
|
syl5bb |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) <-> ( ( v e. RR /\ C < v /\ v < ( B + 1 ) ) /\ ( v e. RR /\ A <_ v /\ v <_ B ) ) ) ) |
61 |
46 51 60
|
3bitr4d |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( v e. ( C (,] B ) <-> v e. ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) ) |
62 |
61
|
eqrdv |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) |
63 |
|
ineq1 |
|- ( v = ( C (,) ( B + 1 ) ) -> ( v i^i ( A [,] B ) ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) |
64 |
63
|
rspceeqv |
|- ( ( ( C (,) ( B + 1 ) ) e. ( topGen ` ran (,) ) /\ ( C (,] B ) = ( ( C (,) ( B + 1 ) ) i^i ( A [,] B ) ) ) -> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) ) |
65 |
2 62 64
|
sylancr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) ) |
66 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
67 |
|
ovex |
|- ( A [,] B ) e. _V |
68 |
|
elrest |
|- ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) <-> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) ) ) |
69 |
66 67 68
|
mp2an |
|- ( ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) <-> E. v e. ( topGen ` ran (,) ) ( C (,] B ) = ( v i^i ( A [,] B ) ) ) |
70 |
65 69
|
sylibr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) |
71 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
72 |
71
|
adantr |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( A [,] B ) C_ RR ) |
73 |
|
eqid |
|- ( topGen ` ran (,) ) = ( topGen ` ran (,) ) |
74 |
73 1
|
resubmet |
|- ( ( A [,] B ) C_ RR -> J = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) |
75 |
72 74
|
syl |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> J = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) |
76 |
70 75
|
eleqtrrd |
|- ( ( ( A e. RR /\ B e. RR ) /\ C e. ( A [,) B ) ) -> ( C (,] B ) e. J ) |
77 |
76
|
ex |
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) -> ( C (,] B ) e. J ) ) |