Step |
Hyp |
Ref |
Expression |
1 |
|
icccmp.1 |
|- J = ( topGen ` ran (,) ) |
2 |
|
icccmp.2 |
|- T = ( J |`t ( A [,] B ) ) |
3 |
|
eqid |
|- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) ) |
4 |
|
eqid |
|- { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } = { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } |
5 |
|
simplll |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> A e. RR ) |
6 |
|
simpllr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> B e. RR ) |
7 |
|
simplr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> A <_ B ) |
8 |
|
elpwi |
|- ( u e. ~P J -> u C_ J ) |
9 |
8
|
ad2antrl |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> u C_ J ) |
10 |
|
simprr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> ( A [,] B ) C_ U. u ) |
11 |
1 2 3 4 5 6 7 9 10
|
icccmplem3 |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } ) |
12 |
|
oveq2 |
|- ( x = B -> ( A [,] x ) = ( A [,] B ) ) |
13 |
12
|
sseq1d |
|- ( x = B -> ( ( A [,] x ) C_ U. z <-> ( A [,] B ) C_ U. z ) ) |
14 |
13
|
rexbidv |
|- ( x = B -> ( E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z <-> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) |
15 |
14
|
elrab |
|- ( B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } <-> ( B e. ( A [,] B ) /\ E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) |
16 |
15
|
simprbi |
|- ( B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) |
17 |
11 16
|
syl |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) |
18 |
17
|
expr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ u e. ~P J ) -> ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) |
19 |
18
|
ralrimiva |
|- ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) |
20 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
21 |
1 20
|
eqeltri |
|- J e. Top |
22 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
23 |
22
|
adantr |
|- ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( A [,] B ) C_ RR ) |
24 |
|
uniretop |
|- RR = U. ( topGen ` ran (,) ) |
25 |
1
|
unieqi |
|- U. J = U. ( topGen ` ran (,) ) |
26 |
24 25
|
eqtr4i |
|- RR = U. J |
27 |
26
|
cmpsub |
|- ( ( J e. Top /\ ( A [,] B ) C_ RR ) -> ( ( J |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) ) |
28 |
21 23 27
|
sylancr |
|- ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( J |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) ) |
29 |
19 28
|
mpbird |
|- ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( J |`t ( A [,] B ) ) e. Comp ) |
30 |
|
rexr |
|- ( A e. RR -> A e. RR* ) |
31 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
32 |
|
icc0 |
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) ) |
33 |
30 31 32
|
syl2an |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A [,] B ) = (/) <-> B < A ) ) |
34 |
33
|
biimpar |
|- ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( A [,] B ) = (/) ) |
35 |
34
|
oveq2d |
|- ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) = ( J |`t (/) ) ) |
36 |
|
rest0 |
|- ( J e. Top -> ( J |`t (/) ) = { (/) } ) |
37 |
21 36
|
ax-mp |
|- ( J |`t (/) ) = { (/) } |
38 |
35 37
|
eqtrdi |
|- ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) = { (/) } ) |
39 |
|
0cmp |
|- { (/) } e. Comp |
40 |
38 39
|
eqeltrdi |
|- ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) e. Comp ) |
41 |
|
lelttric |
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) ) |
42 |
29 40 41
|
mpjaodan |
|- ( ( A e. RR /\ B e. RR ) -> ( J |`t ( A [,] B ) ) e. Comp ) |
43 |
2 42
|
eqeltrid |
|- ( ( A e. RR /\ B e. RR ) -> T e. Comp ) |