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