Step |
Hyp |
Ref |
Expression |
1 |
|
biimp |
|- ( ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> ( ( u X. { x } ) C_ M -> ( u X. { t } ) C_ M ) ) |
2 |
|
iitop |
|- II e. Top |
3 |
|
iiuni |
|- ( 0 [,] 1 ) = U. II |
4 |
3
|
neii1 |
|- ( ( II e. Top /\ u e. ( ( nei ` II ) ` { y } ) ) -> u C_ ( 0 [,] 1 ) ) |
5 |
2 4
|
mpan |
|- ( u e. ( ( nei ` II ) ` { y } ) -> u C_ ( 0 [,] 1 ) ) |
6 |
5
|
adantl |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> u C_ ( 0 [,] 1 ) ) |
7 |
|
xpss1 |
|- ( u C_ ( 0 [,] 1 ) -> ( u X. { x } ) C_ ( ( 0 [,] 1 ) X. { x } ) ) |
8 |
6 7
|
syl |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( u X. { x } ) C_ ( ( 0 [,] 1 ) X. { x } ) ) |
9 |
|
simpl |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( ( 0 [,] 1 ) X. { x } ) C_ M ) |
10 |
8 9
|
sstrd |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( u X. { x } ) C_ M ) |
11 |
|
ssnei |
|- ( ( II e. Top /\ u e. ( ( nei ` II ) ` { y } ) ) -> { y } C_ u ) |
12 |
2 11
|
mpan |
|- ( u e. ( ( nei ` II ) ` { y } ) -> { y } C_ u ) |
13 |
12
|
adantl |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> { y } C_ u ) |
14 |
|
vex |
|- y e. _V |
15 |
14
|
snss |
|- ( y e. u <-> { y } C_ u ) |
16 |
13 15
|
sylibr |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> y e. u ) |
17 |
|
vsnid |
|- t e. { t } |
18 |
|
opelxpi |
|- ( ( y e. u /\ t e. { t } ) -> <. y , t >. e. ( u X. { t } ) ) |
19 |
16 17 18
|
sylancl |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> <. y , t >. e. ( u X. { t } ) ) |
20 |
|
ssel |
|- ( ( u X. { t } ) C_ M -> ( <. y , t >. e. ( u X. { t } ) -> <. y , t >. e. M ) ) |
21 |
19 20
|
syl5com |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( ( u X. { t } ) C_ M -> <. y , t >. e. M ) ) |
22 |
10 21
|
embantd |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( ( ( u X. { x } ) C_ M -> ( u X. { t } ) C_ M ) -> <. y , t >. e. M ) ) |
23 |
1 22
|
syl5 |
|- ( ( ( ( 0 [,] 1 ) X. { x } ) C_ M /\ u e. ( ( nei ` II ) ` { y } ) ) -> ( ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> <. y , t >. e. M ) ) |
24 |
23
|
rexlimdva |
|- ( ( ( 0 [,] 1 ) X. { x } ) C_ M -> ( E. u e. ( ( nei ` II ) ` { y } ) ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> <. y , t >. e. M ) ) |
25 |
24
|
ralimdv |
|- ( ( ( 0 [,] 1 ) X. { x } ) C_ M -> ( A. y e. ( 0 [,] 1 ) E. u e. ( ( nei ` II ) ` { y } ) ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> A. y e. ( 0 [,] 1 ) <. y , t >. e. M ) ) |
26 |
25
|
com12 |
|- ( A. y e. ( 0 [,] 1 ) E. u e. ( ( nei ` II ) ` { y } ) ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> ( ( ( 0 [,] 1 ) X. { x } ) C_ M -> A. y e. ( 0 [,] 1 ) <. y , t >. e. M ) ) |
27 |
|
dfss3 |
|- ( ( ( 0 [,] 1 ) X. { t } ) C_ M <-> A. z e. ( ( 0 [,] 1 ) X. { t } ) z e. M ) |
28 |
|
eleq1 |
|- ( z = <. y , u >. -> ( z e. M <-> <. y , u >. e. M ) ) |
29 |
28
|
ralxp |
|- ( A. z e. ( ( 0 [,] 1 ) X. { t } ) z e. M <-> A. y e. ( 0 [,] 1 ) A. u e. { t } <. y , u >. e. M ) |
30 |
|
vex |
|- t e. _V |
31 |
|
opeq2 |
|- ( u = t -> <. y , u >. = <. y , t >. ) |
32 |
31
|
eleq1d |
|- ( u = t -> ( <. y , u >. e. M <-> <. y , t >. e. M ) ) |
33 |
30 32
|
ralsn |
|- ( A. u e. { t } <. y , u >. e. M <-> <. y , t >. e. M ) |
34 |
33
|
ralbii |
|- ( A. y e. ( 0 [,] 1 ) A. u e. { t } <. y , u >. e. M <-> A. y e. ( 0 [,] 1 ) <. y , t >. e. M ) |
35 |
27 29 34
|
3bitri |
|- ( ( ( 0 [,] 1 ) X. { t } ) C_ M <-> A. y e. ( 0 [,] 1 ) <. y , t >. e. M ) |
36 |
26 35
|
syl6ibr |
|- ( A. y e. ( 0 [,] 1 ) E. u e. ( ( nei ` II ) ` { y } ) ( ( u X. { x } ) C_ M <-> ( u X. { t } ) C_ M ) -> ( ( ( 0 [,] 1 ) X. { x } ) C_ M -> ( ( 0 [,] 1 ) X. { t } ) C_ M ) ) |