Metamath Proof Explorer

Theorem cvmlift2lem6

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-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 ) )
Assertion cvmlift2lem6 
|- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) )

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 1 2 3 4 5 6 7 cvmlift2lem5 
 |-  ( ph -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
9 8 adantr 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
10 9 ffnd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> K Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
11 fnov 
 |-  ( K Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) <-> K = ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) )
12 10 11 sylib 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> K = ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) )
13 12 reseq1d 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) = ( ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) |` ( { X } X. ( 0 [,] 1 ) ) ) )
14 simpr 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> X e. ( 0 [,] 1 ) )
15 14 snssd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> { X } C_ ( 0 [,] 1 ) )
16 ssid 
 |-  ( 0 [,] 1 ) C_ ( 0 [,] 1 )
17 resmpo 
 |-  ( ( { X } C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ ( 0 [,] 1 ) ) -> ( ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) |` ( { X } X. ( 0 [,] 1 ) ) ) = ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( u K v ) ) )
18 15 16 17 sylancl 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) |` ( { X } X. ( 0 [,] 1 ) ) ) = ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( u K v ) ) )
19 elsni 
 |-  ( u e. { X } -> u = X )
20 19 3ad2ant2 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> u = X )
21 20 oveq1d 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> ( u K v ) = ( X K v ) )
22 simp1r 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> X e. ( 0 [,] 1 ) )
23 simp3 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> v e. ( 0 [,] 1 ) )
24 1 2 3 4 5 6 7 cvmlift2lem4 
 |-  ( ( X e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( X K v ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) )
25 22 23 24 syl2anc 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> ( X K v ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) )
26 21 25 eqtrd 
 |-  ( ( ( ph /\ X e. ( 0 [,] 1 ) ) /\ u e. { X } /\ v e. ( 0 [,] 1 ) ) -> ( u K v ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) )
27 26 mpoeq3dva 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( u K v ) ) = ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) )
28 18 27 eqtrd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u K v ) ) |` ( { X } X. ( 0 [,] 1 ) ) ) = ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) )
29 13 28 eqtrd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) = ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) )
30 eqid 
 |-  ( II |`t { X } ) = ( II |`t { X } )
31 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
32 31 a1i 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
33 eqid 
 |-  ( II |`t ( 0 [,] 1 ) ) = ( II |`t ( 0 [,] 1 ) )
34 16 a1i 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( 0 [,] 1 ) C_ ( 0 [,] 1 ) )
35 32 32 cnmpt2nd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> v ) e. ( ( II tX II ) Cn II ) )
36 eqid 
 |-  ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) )
37 1 2 3 4 5 6 36 cvmlift2lem3 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) e. ( II Cn C ) /\ ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` 0 ) = ( H ` X ) ) )
38 37 simp1d 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) e. ( II Cn C ) )
39 32 32 35 38 cnmpt21f 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) e. ( ( II tX II ) Cn C ) )
40 30 32 15 33 32 34 39 cnmpt2res 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) e. ( ( ( II |`t { X } ) tX ( II |`t ( 0 [,] 1 ) ) ) Cn C ) )
41 iitop 
 |-  II e. Top
42 snex 
 |-  { X } e. _V
43 ovex 
 |-  ( 0 [,] 1 ) e. _V
44 txrest 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( { X } e. _V /\ ( 0 [,] 1 ) e. _V ) ) -> ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) = ( ( II |`t { X } ) tX ( II |`t ( 0 [,] 1 ) ) ) )
45 41 41 42 43 44 mp4an 
 |-  ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) = ( ( II |`t { X } ) tX ( II |`t ( 0 [,] 1 ) ) )
46 45 oveq1i 
 |-  ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) = ( ( ( II |`t { X } ) tX ( II |`t ( 0 [,] 1 ) ) ) Cn C )
47 40 46 eleqtrrdi 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( u e. { X } , v e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` v ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) )
48 29 47 eqeltrd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) )