Metamath Proof Explorer

Theorem cvmlift2lem1

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Assertion cvmlift2lem1 
|- ( 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 ) )

Proof

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 imbitrrdi 
 |-  ( 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 ) )