Metamath Proof Explorer


Theorem cvmlift3lem7

Description: Lemma for cvmlift3 . (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b B = C
cvmlift3.y Y = K
cvmlift3.f φ F C CovMap J
cvmlift3.k φ K SConn
cvmlift3.l φ K N-Locally PConn
cvmlift3.o φ O Y
cvmlift3.g φ G K Cn J
cvmlift3.p φ P B
cvmlift3.e φ F P = G O
cvmlift3.h H = x Y ι z B | f II Cn K f 0 = O f 1 = x ι g II Cn C | F g = G f g 0 = P 1 = z
cvmlift3lem7.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
cvmlift3lem7.1 φ G X A
cvmlift3lem7.2 φ T S A
cvmlift3lem7.3 φ M G -1 A
cvmlift3lem7.w W = ι b T | H X b
cvmlift3lem7.7 φ K 𝑡 M PConn
cvmlift3lem7.4 φ V K
cvmlift3lem7.5 φ V M
cvmlift3lem7.6 φ X V
Assertion cvmlift3lem7 φ H K CnP C X

Proof

Step Hyp Ref Expression
1 cvmlift3.b B = C
2 cvmlift3.y Y = K
3 cvmlift3.f φ F C CovMap J
4 cvmlift3.k φ K SConn
5 cvmlift3.l φ K N-Locally PConn
6 cvmlift3.o φ O Y
7 cvmlift3.g φ G K Cn J
8 cvmlift3.p φ P B
9 cvmlift3.e φ F P = G O
10 cvmlift3.h H = x Y ι z B | f II Cn K f 0 = O f 1 = x ι g II Cn C | F g = G f g 0 = P 1 = z
11 cvmlift3lem7.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
12 cvmlift3lem7.1 φ G X A
13 cvmlift3lem7.2 φ T S A
14 cvmlift3lem7.3 φ M G -1 A
15 cvmlift3lem7.w W = ι b T | H X b
16 cvmlift3lem7.7 φ K 𝑡 M PConn
17 cvmlift3lem7.4 φ V K
18 cvmlift3lem7.5 φ V M
19 cvmlift3lem7.6 φ X V
20 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 φ H : Y B
21 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 φ F H = G
22 21 7 eqeltrd φ F H K Cn J
23 sconntop K SConn K Top
24 4 23 syl φ K Top
25 cnvimass G -1 A dom G
26 eqid J = J
27 2 26 cnf G K Cn J G : Y J
28 fdm G : Y J dom G = Y
29 7 27 28 3syl φ dom G = Y
30 25 29 sseqtrid φ G -1 A Y
31 14 30 sstrd φ M Y
32 18 19 sseldd φ X M
33 31 32 sseldd φ X Y
34 20 33 ffvelrnd φ H X B
35 fvco3 H : Y B X Y F H X = F H X
36 20 33 35 syl2anc φ F H X = F H X
37 21 fveq1d φ F H X = G X
38 36 37 eqtr3d φ F H X = G X
39 38 12 eqeltrd φ F H X A
40 11 1 15 cvmsiota F C CovMap J T S A H X B F H X A W T H X W
41 3 13 34 39 40 syl13anc φ W T H X W
42 eqid H X = H X
43 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 φ X Y H X = H X f II Cn K f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X
44 42 43 mpbii φ X Y f II Cn K f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X
45 33 44 mpdan φ f II Cn K f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X
46 45 adantr φ y M f II Cn K f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X
47 fveq1 f = h f 0 = h 0
48 47 eqeq1d f = h f 0 = O h 0 = O
49 fveq1 f = h f 1 = h 1
50 49 eqeq1d f = h f 1 = X h 1 = X
51 coeq2 f = h G f = G h
52 51 eqeq2d f = h F g = G f F g = G h
53 52 anbi1d f = h F g = G f g 0 = P F g = G h g 0 = P
54 53 riotabidv f = h ι g II Cn C | F g = G f g 0 = P = ι g II Cn C | F g = G h g 0 = P
55 coeq2 a = g F a = F g
56 55 eqeq1d a = g F a = G h F g = G h
57 fveq1 a = g a 0 = g 0
58 57 eqeq1d a = g a 0 = P g 0 = P
59 56 58 anbi12d a = g F a = G h a 0 = P F g = G h g 0 = P
60 59 cbvriotav ι a II Cn C | F a = G h a 0 = P = ι g II Cn C | F g = G h g 0 = P
61 54 60 syl6eqr f = h ι g II Cn C | F g = G f g 0 = P = ι a II Cn C | F a = G h a 0 = P
62 61 fveq1d f = h ι g II Cn C | F g = G f g 0 = P 1 = ι a II Cn C | F a = G h a 0 = P 1
63 62 eqeq1d f = h ι g II Cn C | F g = G f g 0 = P 1 = H X ι a II Cn C | F a = G h a 0 = P 1 = H X
64 48 50 63 3anbi123d f = h f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X
65 64 cbvrexv f II Cn K f 0 = O f 1 = X ι g II Cn C | F g = G f g 0 = P 1 = H X h II Cn K h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X
66 46 65 sylib φ y M h II Cn K h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X
67 16 adantr φ y M K 𝑡 M PConn
68 2 restuni K Top M Y M = K 𝑡 M
69 24 31 68 syl2anc φ M = K 𝑡 M
70 32 69 eleqtrd φ X K 𝑡 M
71 70 adantr φ y M X K 𝑡 M
72 69 eleq2d φ y M y K 𝑡 M
73 72 biimpa φ y M y K 𝑡 M
74 eqid K 𝑡 M = K 𝑡 M
75 74 pconncn K 𝑡 M PConn X K 𝑡 M y K 𝑡 M n II Cn K 𝑡 M n 0 = X n 1 = y
76 67 71 73 75 syl3anc φ y M n II Cn K 𝑡 M n 0 = X n 1 = y
77 reeanv h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y h II Cn K h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n II Cn K 𝑡 M n 0 = X n 1 = y
78 3 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y F C CovMap J
79 4 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y K SConn
80 5 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y K N-Locally PConn
81 6 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y O Y
82 7 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y G K Cn J
83 8 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y P B
84 9 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y F P = G O
85 12 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y G X A
86 13 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y T S A
87 14 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y M G -1 A
88 32 ad3antrrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y X M
89 simpllr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y y M
90 simplrl φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y h II Cn K
91 simprl φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X
92 simplrr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y n II Cn K 𝑡 M
93 simprr φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y n 0 = X n 1 = y
94 55 eqeq1d a = g F a = G n F g = G n
95 57 eqeq1d a = g a 0 = H X g 0 = H X
96 94 95 anbi12d a = g F a = G n a 0 = H X F g = G n g 0 = H X
97 96 cbvriotav ι a II Cn C | F a = G n a 0 = H X = ι g II Cn C | F g = G n g 0 = H X
98 1 2 78 79 80 81 82 83 84 10 11 85 86 87 15 88 89 90 60 91 92 93 97 cvmlift3lem6 φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y H y W
99 98 ex φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y H y W
100 99 rexlimdvva φ y M h II Cn K n II Cn K 𝑡 M h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n 0 = X n 1 = y H y W
101 77 100 syl5bir φ y M h II Cn K h 0 = O h 1 = X ι a II Cn C | F a = G h a 0 = P 1 = H X n II Cn K 𝑡 M n 0 = X n 1 = y H y W
102 66 76 101 mp2and φ y M H y W
103 102 ralrimiva φ y M H y W
104 20 ffund φ Fun H
105 20 fdmd φ dom H = Y
106 31 105 sseqtrrd φ M dom H
107 funimass4 Fun H M dom H H M W y M H y W
108 104 106 107 syl2anc φ H M W y M H y W
109 103 108 mpbird φ H M W
110 1 2 11 3 20 22 24 33 13 41 31 109 cvmlift2lem9a φ H M K 𝑡 M Cn C
111 74 cncnpi H M K 𝑡 M Cn C X K 𝑡 M H M K 𝑡 M CnP C X
112 110 70 111 syl2anc φ H M K 𝑡 M CnP C X
113 2 ssntr K Top M Y V K V M V int K M
114 24 31 17 18 113 syl22anc φ V int K M
115 114 19 sseldd φ X int K M
116 2 1 cnprest K Top M Y X int K M H : Y B H K CnP C X H M K 𝑡 M CnP C X
117 24 31 115 20 116 syl22anc φ H K CnP C X H M K 𝑡 M CnP C X
118 112 117 mpbird φ H K CnP C X