Metamath Proof Explorer

Theorem cvmlift2lem11

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

Ref Expression
Hypotheses cvmlift2.b 
|- B = U. C
cvmlift2.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift2.g 
|- ( ph -> G e. ( ( II tX II ) Cn J ) )
cvmlift2.p 
|- ( ph -> P e. B )
cvmlift2.i 
|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
cvmlift2.h 
|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
cvmlift2.k 
|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
cvmlift2.m 
|- M = { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) }
cvmlift2lem11.1 
|- ( ph -> U e. II )
cvmlift2lem11.2 
|- ( ph -> V e. II )
cvmlift2lem11.3 
|- ( ph -> Y e. V )
cvmlift2lem11.4 
|- ( ph -> Z e. V )
cvmlift2lem11.5 
|- ( ph -> ( E. w e. V ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) ) )
Assertion cvmlift2lem11 
|- ( ph -> ( ( U X. { Y } ) C_ M -> ( U X. { Z } ) C_ M ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b 
 |-  B = U. C
2 cvmlift2.f 
 |-  ( ph -> F e. ( C CovMap J ) )
3 cvmlift2.g 
 |-  ( ph -> G e. ( ( II tX II ) Cn J ) )
4 cvmlift2.p 
 |-  ( ph -> P e. B )
5 cvmlift2.i 
 |-  ( ph -> ( F ` P ) = ( 0 G 0 ) )
6 cvmlift2.h 
 |-  H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
7 cvmlift2.k 
 |-  K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
8 cvmlift2.m 
 |-  M = { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) }
9 cvmlift2lem11.1 
 |-  ( ph -> U e. II )
10 cvmlift2lem11.2 
 |-  ( ph -> V e. II )
11 cvmlift2lem11.3 
 |-  ( ph -> Y e. V )
12 cvmlift2lem11.4 
 |-  ( ph -> Z e. V )
13 cvmlift2lem11.5 
 |-  ( ph -> ( E. w e. V ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) ) )
14 9 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> U e. II )
15 elssuni 
 |-  ( U e. II -> U C_ U. II )
16 iiuni 
 |-  ( 0 [,] 1 ) = U. II
17 15 16 sseqtrrdi 
 |-  ( U e. II -> U C_ ( 0 [,] 1 ) )
18 14 17 syl 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> U C_ ( 0 [,] 1 ) )
19 elunii 
 |-  ( ( Z e. V /\ V e. II ) -> Z e. U. II )
20 19 16 eleqtrrdi 
 |-  ( ( Z e. V /\ V e. II ) -> Z e. ( 0 [,] 1 ) )
21 12 10 20 syl2anc 
 |-  ( ph -> Z e. ( 0 [,] 1 ) )
22 21 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> Z e. ( 0 [,] 1 ) )
23 22 snssd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> { Z } C_ ( 0 [,] 1 ) )
24 xpss12 
 |-  ( ( U C_ ( 0 [,] 1 ) /\ { Z } C_ ( 0 [,] 1 ) ) -> ( U X. { Z } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
25 18 23 24 syl2anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
26 11 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> Y e. V )
27 1 2 3 4 5 6 7 cvmlift2lem5 
 |-  ( ph -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
28 27 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
29 10 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> V e. II )
30 elssuni 
 |-  ( V e. II -> V C_ U. II )
31 30 16 sseqtrrdi 
 |-  ( V e. II -> V C_ ( 0 [,] 1 ) )
32 29 31 syl 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> V C_ ( 0 [,] 1 ) )
33 32 26 sseldd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> Y e. ( 0 [,] 1 ) )
34 33 snssd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> { Y } C_ ( 0 [,] 1 ) )
35 xpss12 
 |-  ( ( U C_ ( 0 [,] 1 ) /\ { Y } C_ ( 0 [,] 1 ) ) -> ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
36 18 34 35 syl2anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
37 28 36 fssresd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( K |` ( U X. { Y } ) ) : ( U X. { Y } ) --> B )
38 36 adantr 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Y } ) ) -> ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
39 simpr 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Y } ) ) -> z e. ( U X. { Y } ) )
40 simpr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Y } ) C_ M )
41 40 8 sseqtrdi 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Y } ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } )
42 ssrab 
 |-  ( ( U X. { Y } ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } <-> ( ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ A. z e. ( U X. { Y } ) K e. ( ( ( II tX II ) CnP C ) ` z ) ) )
43 42 simprbi 
 |-  ( ( U X. { Y } ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } -> A. z e. ( U X. { Y } ) K e. ( ( ( II tX II ) CnP C ) ` z ) )
44 41 43 syl 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> A. z e. ( U X. { Y } ) K e. ( ( ( II tX II ) CnP C ) ` z ) )
45 44 r19.21bi 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Y } ) ) -> K e. ( ( ( II tX II ) CnP C ) ` z ) )
46 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
47 txtopon 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ II e. ( TopOn ` ( 0 [,] 1 ) ) ) -> ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
48 46 46 47 mp2an 
 |-  ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
49 48 toponunii 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II )
50 49 cnpresti 
 |-  ( ( ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ z e. ( U X. { Y } ) /\ K e. ( ( ( II tX II ) CnP C ) ` z ) ) -> ( K |` ( U X. { Y } ) ) e. ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) CnP C ) ` z ) )
51 38 39 45 50 syl3anc 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Y } ) ) -> ( K |` ( U X. { Y } ) ) e. ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) CnP C ) ` z ) )
52 51 ralrimiva 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> A. z e. ( U X. { Y } ) ( K |` ( U X. { Y } ) ) e. ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) CnP C ) ` z ) )
53 resttopon 
 |-  ( ( ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) /\ ( U X. { Y } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( ( II tX II ) |`t ( U X. { Y } ) ) e. ( TopOn ` ( U X. { Y } ) ) )
54 48 36 53 sylancr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( ( II tX II ) |`t ( U X. { Y } ) ) e. ( TopOn ` ( U X. { Y } ) ) )
55 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
56 2 55 syl 
 |-  ( ph -> C e. Top )
57 56 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> C e. Top )
58 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
59 57 58 sylib 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> C e. ( TopOn ` B ) )
60 cncnp 
 |-  ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) e. ( TopOn ` ( U X. { Y } ) ) /\ C e. ( TopOn ` B ) ) -> ( ( K |` ( U X. { Y } ) ) e. ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) <-> ( ( K |` ( U X. { Y } ) ) : ( U X. { Y } ) --> B /\ A. z e. ( U X. { Y } ) ( K |` ( U X. { Y } ) ) e. ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) CnP C ) ` z ) ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( ( K |` ( U X. { Y } ) ) e. ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) <-> ( ( K |` ( U X. { Y } ) ) : ( U X. { Y } ) --> B /\ A. z e. ( U X. { Y } ) ( K |` ( U X. { Y } ) ) e. ( ( ( ( II tX II ) |`t ( U X. { Y } ) ) CnP C ) ` z ) ) ) )
62 37 52 61 mpbir2and 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( K |` ( U X. { Y } ) ) e. ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) )
63 sneq 
 |-  ( w = Y -> { w } = { Y } )
64 63 xpeq2d 
 |-  ( w = Y -> ( U X. { w } ) = ( U X. { Y } ) )
65 64 reseq2d 
 |-  ( w = Y -> ( K |` ( U X. { w } ) ) = ( K |` ( U X. { Y } ) ) )
66 64 oveq2d 
 |-  ( w = Y -> ( ( II tX II ) |`t ( U X. { w } ) ) = ( ( II tX II ) |`t ( U X. { Y } ) ) )
67 66 oveq1d 
 |-  ( w = Y -> ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) = ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) )
68 65 67 eleq12d 
 |-  ( w = Y -> ( ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) <-> ( K |` ( U X. { Y } ) ) e. ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) ) )
69 68 rspcev 
 |-  ( ( Y e. V /\ ( K |` ( U X. { Y } ) ) e. ( ( ( II tX II ) |`t ( U X. { Y } ) ) Cn C ) ) -> E. w e. V ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) )
70 26 62 69 syl2anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> E. w e. V ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) )
71 13 imp 
 |-  ( ( ph /\ E. w e. V ( K |` ( U X. { w } ) ) e. ( ( ( II tX II ) |`t ( U X. { w } ) ) Cn C ) ) -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) )
72 70 71 syldan 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) )
73 72 adantr 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) )
74 12 adantr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> Z e. V )
75 74 snssd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> { Z } C_ V )
76 xpss2 
 |-  ( { Z } C_ V -> ( U X. { Z } ) C_ ( U X. V ) )
77 75 76 syl 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ ( U X. V ) )
78 iitop 
 |-  II e. Top
79 78 78 txtopi 
 |-  ( II tX II ) e. Top
80 xpss12 
 |-  ( ( U C_ ( 0 [,] 1 ) /\ V C_ ( 0 [,] 1 ) ) -> ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
81 18 32 80 syl2anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
82 49 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( U X. V ) = U. ( ( II tX II ) |`t ( U X. V ) ) )
83 79 81 82 sylancr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. V ) = U. ( ( II tX II ) |`t ( U X. V ) ) )
84 77 83 sseqtrd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ U. ( ( II tX II ) |`t ( U X. V ) ) )
85 84 sselda 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> z e. U. ( ( II tX II ) |`t ( U X. V ) ) )
86 eqid 
 |-  U. ( ( II tX II ) |`t ( U X. V ) ) = U. ( ( II tX II ) |`t ( U X. V ) )
87 86 cncnpi 
 |-  ( ( ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) /\ z e. U. ( ( II tX II ) |`t ( U X. V ) ) ) -> ( K |` ( U X. V ) ) e. ( ( ( ( II tX II ) |`t ( U X. V ) ) CnP C ) ` z ) )
88 73 85 87 syl2anc 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> ( K |` ( U X. V ) ) e. ( ( ( ( II tX II ) |`t ( U X. V ) ) CnP C ) ` z ) )
89 79 a1i 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> ( II tX II ) e. Top )
90 81 adantr 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
91 78 a1i 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> II e. Top )
92 txopn 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( U e. II /\ V e. II ) ) -> ( U X. V ) e. ( II tX II ) )
93 91 91 14 29 92 syl22anc 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. V ) e. ( II tX II ) )
94 isopn3i 
 |-  ( ( ( II tX II ) e. Top /\ ( U X. V ) e. ( II tX II ) ) -> ( ( int ` ( II tX II ) ) ` ( U X. V ) ) = ( U X. V ) )
95 79 93 94 sylancr 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( ( int ` ( II tX II ) ) ` ( U X. V ) ) = ( U X. V ) )
96 77 95 sseqtrrd 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ ( ( int ` ( II tX II ) ) ` ( U X. V ) ) )
97 96 sselda 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> z e. ( ( int ` ( II tX II ) ) ` ( U X. V ) ) )
98 27 ad2antrr 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
99 49 1 cnprest 
 |-  ( ( ( ( II tX II ) e. Top /\ ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) /\ ( z e. ( ( int ` ( II tX II ) ) ` ( U X. V ) ) /\ K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B ) ) -> ( K e. ( ( ( II tX II ) CnP C ) ` z ) <-> ( K |` ( U X. V ) ) e. ( ( ( ( II tX II ) |`t ( U X. V ) ) CnP C ) ` z ) ) )
100 89 90 97 98 99 syl22anc 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> ( K e. ( ( ( II tX II ) CnP C ) ` z ) <-> ( K |` ( U X. V ) ) e. ( ( ( ( II tX II ) |`t ( U X. V ) ) CnP C ) ` z ) ) )
101 88 100 mpbird 
 |-  ( ( ( ph /\ ( U X. { Y } ) C_ M ) /\ z e. ( U X. { Z } ) ) -> K e. ( ( ( II tX II ) CnP C ) ` z ) )
102 25 101 ssrabdv 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } )
103 102 8 sseqtrrdi 
 |-  ( ( ph /\ ( U X. { Y } ) C_ M ) -> ( U X. { Z } ) C_ M )
104 103 ex 
 |-  ( ph -> ( ( U X. { Y } ) C_ M -> ( U X. { Z } ) C_ M ) )