Metamath Proof Explorer


Theorem cvmlift2lem6

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b B = C
cvmlift2.f φ F C CovMap J
cvmlift2.g φ G II × t II Cn J
cvmlift2.p φ P B
cvmlift2.i φ F P = 0 G 0
cvmlift2.h H = ι f II Cn C | F f = z 0 1 z G 0 f 0 = P
cvmlift2.k K = x 0 1 , y 0 1 ι f II Cn C | F f = z 0 1 x G z f 0 = H x y
Assertion cvmlift2lem6 φ X 0 1 K X × 0 1 II × t II 𝑡 X × 0 1 Cn C

Proof

Step Hyp Ref Expression
1 cvmlift2.b B = C
2 cvmlift2.f φ F C CovMap J
3 cvmlift2.g φ G II × t II Cn J
4 cvmlift2.p φ P B
5 cvmlift2.i φ F P = 0 G 0
6 cvmlift2.h H = ι f II Cn C | F f = z 0 1 z G 0 f 0 = P
7 cvmlift2.k K = x 0 1 , y 0 1 ι f II Cn C | F f = z 0 1 x G z f 0 = H x y
8 1 2 3 4 5 6 7 cvmlift2lem5 φ K : 0 1 × 0 1 B
9 8 adantr φ X 0 1 K : 0 1 × 0 1 B
10 9 ffnd φ X 0 1 K Fn 0 1 × 0 1
11 fnov K Fn 0 1 × 0 1 K = u 0 1 , v 0 1 u K v
12 10 11 sylib φ X 0 1 K = u 0 1 , v 0 1 u K v
13 12 reseq1d φ X 0 1 K X × 0 1 = u 0 1 , v 0 1 u K v X × 0 1
14 simpr φ X 0 1 X 0 1
15 14 snssd φ X 0 1 X 0 1
16 ssid 0 1 0 1
17 resmpo X 0 1 0 1 0 1 u 0 1 , v 0 1 u K v X × 0 1 = u X , v 0 1 u K v
18 15 16 17 sylancl φ X 0 1 u 0 1 , v 0 1 u K v X × 0 1 = u X , v 0 1 u K v
19 elsni u X u = X
20 19 3ad2ant2 φ X 0 1 u X v 0 1 u = X
21 20 oveq1d φ X 0 1 u X v 0 1 u K v = X K v
22 simp1r φ X 0 1 u X v 0 1 X 0 1
23 simp3 φ X 0 1 u X v 0 1 v 0 1
24 1 2 3 4 5 6 7 cvmlift2lem4 X 0 1 v 0 1 X K v = ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
25 22 23 24 syl2anc φ X 0 1 u X v 0 1 X K v = ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
26 21 25 eqtrd φ X 0 1 u X v 0 1 u K v = ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
27 26 mpoeq3dva φ X 0 1 u X , v 0 1 u K v = u X , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
28 18 27 eqtrd φ X 0 1 u 0 1 , v 0 1 u K v X × 0 1 = u X , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
29 13 28 eqtrd φ X 0 1 K X × 0 1 = u X , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v
30 eqid II 𝑡 X = II 𝑡 X
31 iitopon II TopOn 0 1
32 31 a1i φ X 0 1 II TopOn 0 1
33 eqid II 𝑡 0 1 = II 𝑡 0 1
34 16 a1i φ X 0 1 0 1 0 1
35 32 32 cnmpt2nd φ X 0 1 u 0 1 , v 0 1 v II × t II Cn II
36 eqid ι f II Cn C | F f = z 0 1 X G z f 0 = H X = ι f II Cn C | F f = z 0 1 X G z f 0 = H X
37 1 2 3 4 5 6 36 cvmlift2lem3 φ X 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X II Cn C F ι f II Cn C | F f = z 0 1 X G z f 0 = H X = z 0 1 X G z ι f II Cn C | F f = z 0 1 X G z f 0 = H X 0 = H X
38 37 simp1d φ X 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X II Cn C
39 32 32 35 38 cnmpt21f φ X 0 1 u 0 1 , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v II × t II Cn C
40 30 32 15 33 32 34 39 cnmpt2res φ X 0 1 u X , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v II 𝑡 X × t II 𝑡 0 1 Cn C
41 iitop II Top
42 snex X V
43 ovex 0 1 V
44 txrest II Top II Top X V 0 1 V II × t II 𝑡 X × 0 1 = II 𝑡 X × t II 𝑡 0 1
45 41 41 42 43 44 mp4an II × t II 𝑡 X × 0 1 = II 𝑡 X × t II 𝑡 0 1
46 45 oveq1i II × t II 𝑡 X × 0 1 Cn C = II 𝑡 X × t II 𝑡 0 1 Cn C
47 40 46 syl6eleqr φ X 0 1 u X , v 0 1 ι f II Cn C | F f = z 0 1 X G z f 0 = H X v II × t II 𝑡 X × 0 1 Cn C
48 29 47 eqeltrd φ X 0 1 K X × 0 1 II × t II 𝑡 X × 0 1 Cn C