Metamath Proof Explorer


Theorem cvmlift2lem12

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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
cvmlift2.m M = z 0 1 × 0 1 | K II × t II CnP C z
cvmlift2.a A = a 0 1 | 0 1 × a M
cvmlift2.s S = r t | t 0 1 u nei II r u × a M u × t M
Assertion cvmlift2lem12 φ K II × t II 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 cvmlift2.m M = z 0 1 × 0 1 | K II × t II CnP C z
9 cvmlift2.a A = a 0 1 | 0 1 × a M
10 cvmlift2.s S = r t | t 0 1 u nei II r u × a M u × t M
11 1 2 3 4 5 6 7 cvmlift2lem5 φ K : 0 1 × 0 1 B
12 iunid a 0 1 a = 0 1
13 12 xpeq2i 0 1 × a 0 1 a = 0 1 × 0 1
14 xpiundi 0 1 × a 0 1 a = a 0 1 0 1 × a
15 13 14 eqtr3i 0 1 × 0 1 = a 0 1 0 1 × a
16 iiuni 0 1 = II
17 iiconn II Conn
18 17 a1i φ II Conn
19 inss1 II Clsd II II
20 iicmp II Comp
21 20 a1i φ a 0 1 II Comp
22 iitop II Top
23 22 a1i φ a 0 1 II Top
24 22 22 txtopi II × t II Top
25 16 neiss2 II Top u nei II r r 0 1
26 22 25 mpan u nei II r r 0 1
27 vex r V
28 27 snss r 0 1 r 0 1
29 26 28 sylibr u nei II r r 0 1
30 29 a1d u nei II r u × a M u × t M r 0 1
31 30 rexlimiv u nei II r u × a M u × t M r 0 1
32 31 adantl t 0 1 u nei II r u × a M u × t M r 0 1
33 simpl t 0 1 u nei II r u × a M u × t M t 0 1
34 32 33 jca t 0 1 u nei II r u × a M u × t M r 0 1 t 0 1
35 34 ssopab2i r t | t 0 1 u nei II r u × a M u × t M r t | r 0 1 t 0 1
36 df-xp 0 1 × 0 1 = r t | r 0 1 t 0 1
37 35 10 36 3sstr4i S 0 1 × 0 1
38 22 22 16 16 txunii 0 1 × 0 1 = II × t II
39 38 ntropn II × t II Top S 0 1 × 0 1 int II × t II S II × t II
40 24 37 39 mp2an int II × t II S II × t II
41 40 a1i φ a 0 1 int II × t II S II × t II
42 2 adantr φ a 0 1 b 0 1 F C CovMap J
43 3 adantr φ a 0 1 b 0 1 G II × t II Cn J
44 4 adantr φ a 0 1 b 0 1 P B
45 5 adantr φ a 0 1 b 0 1 F P = 0 G 0
46 eqid k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
47 simprr φ a 0 1 b 0 1 b 0 1
48 simprl φ a 0 1 b 0 1 a 0 1
49 1 42 43 44 45 6 7 46 47 48 cvmlift2lem10 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C
50 24 a1i φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C II × t II Top
51 37 a1i φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C S 0 1 × 0 1
52 22 a1i φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C II Top
53 simplrl φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C u II
54 simplrr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C v II
55 txopn II Top II Top u II v II u × v II × t II
56 52 52 53 54 55 syl22anc φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C u × v II × t II
57 simpr r u t v t v
58 elunii t v v II t II
59 58 16 eleqtrrdi t v v II t 0 1
60 57 54 59 syl2anr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v t 0 1
61 22 a1i φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v II Top
62 53 adantr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u II
63 simprl φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v r u
64 opnneip II Top u II r u u nei II r
65 61 62 63 64 syl3anc φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u nei II r
66 42 ad3antrrr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v F C CovMap J
67 43 ad3antrrr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v G II × t II Cn J
68 44 ad3antrrr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v P B
69 45 ad3antrrr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v F P = 0 G 0
70 54 adantr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v v II
71 simplr2 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v a v
72 simprr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v t v
73 sneq c = w c = w
74 73 xpeq2d c = w u × c = u × w
75 74 reseq2d c = w K u × c = K u × w
76 74 oveq2d c = w II × t II 𝑡 u × c = II × t II 𝑡 u × w
77 76 oveq1d c = w II × t II 𝑡 u × c Cn C = II × t II 𝑡 u × w Cn C
78 75 77 eleq12d c = w K u × c II × t II 𝑡 u × c Cn C K u × w II × t II 𝑡 u × w Cn C
79 78 cbvrexvw c v K u × c II × t II 𝑡 u × c Cn C w v K u × w II × t II 𝑡 u × w Cn C
80 simplr3 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C
81 79 80 syl5bi φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v c v K u × c II × t II 𝑡 u × c Cn C K u × v II × t II 𝑡 u × v Cn C
82 1 66 67 68 69 6 7 8 62 70 71 72 81 cvmlift2lem11 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u × a M u × t M
83 1 66 67 68 69 6 7 8 62 70 72 71 81 cvmlift2lem11 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u × t M u × a M
84 82 83 impbid φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u × a M u × t M
85 rspe u nei II r u × a M u × t M u nei II r u × a M u × t M
86 65 84 85 syl2anc φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v u nei II r u × a M u × t M
87 60 86 jca φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v t 0 1 u nei II r u × a M u × t M
88 87 ex φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u t v t 0 1 u nei II r u × a M u × t M
89 88 alrimivv φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r t r u t v t 0 1 u nei II r u × a M u × t M
90 df-xp u × v = r t | r u t v
91 90 10 sseq12i u × v S r t | r u t v r t | t 0 1 u nei II r u × a M u × t M
92 ssopab2bw r t | r u t v r t | t 0 1 u nei II r u × a M u × t M r t r u t v t 0 1 u nei II r u × a M u × t M
93 91 92 bitri u × v S r t r u t v t 0 1 u nei II r u × a M u × t M
94 89 93 sylibr φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C u × v S
95 38 ssntr II × t II Top S 0 1 × 0 1 u × v II × t II u × v S u × v int II × t II S
96 50 51 56 94 95 syl22anc φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C u × v int II × t II S
97 simpr1 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C b u
98 simpr2 φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C a v
99 opelxpi b u a v b a u × v
100 97 98 99 syl2anc φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C b a u × v
101 96 100 sseldd φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C b a int II × t II S
102 101 ex φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C b a int II × t II S
103 102 rexlimdvva φ a 0 1 b 0 1 u II v II b u a v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C b a int II × t II S
104 49 103 mpd φ a 0 1 b 0 1 b a int II × t II S
105 vex a V
106 opeq2 w = a b w = b a
107 106 eleq1d w = a b w int II × t II S b a int II × t II S
108 105 107 ralsn w a b w int II × t II S b a int II × t II S
109 104 108 sylibr φ a 0 1 b 0 1 w a b w int II × t II S
110 109 anassrs φ a 0 1 b 0 1 w a b w int II × t II S
111 110 ralrimiva φ a 0 1 b 0 1 w a b w int II × t II S
112 dfss3 0 1 × a int II × t II S u 0 1 × a u int II × t II S
113 eleq1 u = b w u int II × t II S b w int II × t II S
114 113 ralxp u 0 1 × a u int II × t II S b 0 1 w a b w int II × t II S
115 112 114 bitri 0 1 × a int II × t II S b 0 1 w a b w int II × t II S
116 111 115 sylibr φ a 0 1 0 1 × a int II × t II S
117 simpr φ a 0 1 a 0 1
118 16 16 21 23 41 116 117 txtube φ a 0 1 v II a v 0 1 × v int II × t II S
119 38 ntrss2 II × t II Top S 0 1 × 0 1 int II × t II S S
120 24 37 119 mp2an int II × t II S S
121 sstr 0 1 × v int II × t II S int II × t II S S 0 1 × v S
122 120 121 mpan2 0 1 × v int II × t II S 0 1 × v S
123 df-xp 0 1 × v = r t | r 0 1 t v
124 123 10 sseq12i 0 1 × v S r t | r 0 1 t v r t | t 0 1 u nei II r u × a M u × t M
125 ssopab2bw r t | r 0 1 t v r t | t 0 1 u nei II r u × a M u × t M r t r 0 1 t v t 0 1 u nei II r u × a M u × t M
126 r2al r 0 1 t v t 0 1 u nei II r u × a M u × t M r t r 0 1 t v t 0 1 u nei II r u × a M u × t M
127 ralcom r 0 1 t v t 0 1 u nei II r u × a M u × t M t v r 0 1 t 0 1 u nei II r u × a M u × t M
128 125 126 127 3bitr2i r t | r 0 1 t v r t | t 0 1 u nei II r u × a M u × t M t v r 0 1 t 0 1 u nei II r u × a M u × t M
129 124 128 bitri 0 1 × v S t v r 0 1 t 0 1 u nei II r u × a M u × t M
130 122 129 sylib 0 1 × v int II × t II S t v r 0 1 t 0 1 u nei II r u × a M u × t M
131 simpr t 0 1 u nei II r u × a M u × t M u nei II r u × a M u × t M
132 131 ralimi r 0 1 t 0 1 u nei II r u × a M u × t M r 0 1 u nei II r u × a M u × t M
133 cvmlift2lem1 r 0 1 u nei II r u × a M u × t M 0 1 × a M 0 1 × t M
134 bicom u × a M u × t M u × t M u × a M
135 134 rexbii u nei II r u × a M u × t M u nei II r u × t M u × a M
136 135 ralbii r 0 1 u nei II r u × a M u × t M r 0 1 u nei II r u × t M u × a M
137 cvmlift2lem1 r 0 1 u nei II r u × t M u × a M 0 1 × t M 0 1 × a M
138 136 137 sylbi r 0 1 u nei II r u × a M u × t M 0 1 × t M 0 1 × a M
139 133 138 impbid r 0 1 u nei II r u × a M u × t M 0 1 × a M 0 1 × t M
140 132 139 syl r 0 1 t 0 1 u nei II r u × a M u × t M 0 1 × a M 0 1 × t M
141 9 rabeq2i a A a 0 1 0 1 × a M
142 141 baib a 0 1 a A 0 1 × a M
143 142 ad3antlr φ a 0 1 v II t v a A 0 1 × a M
144 elssuni v II v II
145 144 16 sseqtrrdi v II v 0 1
146 145 adantl φ a 0 1 v II v 0 1
147 146 sselda φ a 0 1 v II t v t 0 1
148 sneq a = t a = t
149 148 xpeq2d a = t 0 1 × a = 0 1 × t
150 149 sseq1d a = t 0 1 × a M 0 1 × t M
151 150 9 elrab2 t A t 0 1 0 1 × t M
152 151 baib t 0 1 t A 0 1 × t M
153 147 152 syl φ a 0 1 v II t v t A 0 1 × t M
154 143 153 bibi12d φ a 0 1 v II t v a A t A 0 1 × a M 0 1 × t M
155 140 154 syl5ibr φ a 0 1 v II t v r 0 1 t 0 1 u nei II r u × a M u × t M a A t A
156 155 ralimdva φ a 0 1 v II t v r 0 1 t 0 1 u nei II r u × a M u × t M t v a A t A
157 130 156 syl5 φ a 0 1 v II 0 1 × v int II × t II S t v a A t A
158 157 anim2d φ a 0 1 v II a v 0 1 × v int II × t II S a v t v a A t A
159 158 reximdva φ a 0 1 v II a v 0 1 × v int II × t II S v II a v t v a A t A
160 118 159 mpd φ a 0 1 v II a v t v a A t A
161 160 ralrimiva φ a 0 1 v II a v t v a A t A
162 ssrab2 a 0 1 | 0 1 × a M 0 1
163 9 162 eqsstri A 0 1
164 16 isclo II Top A 0 1 A II Clsd II a 0 1 v II a v t v a A t A
165 22 163 164 mp2an A II Clsd II a 0 1 v II a v t v a A t A
166 161 165 sylibr φ A II Clsd II
167 19 166 sseldi φ A II
168 0elunit 0 0 1
169 168 a1i φ 0 0 1
170 relxp Rel 0 1 × 0
171 170 a1i φ Rel 0 1 × 0
172 opelxp r a 0 1 × 0 r 0 1 a 0
173 id r 0 1 r 0 1
174 opelxpi r 0 1 0 0 1 r 0 0 1 × 0 1
175 173 169 174 syl2anr φ r 0 1 r 0 0 1 × 0 1
176 2 adantr φ r 0 1 F C CovMap J
177 3 adantr φ r 0 1 G II × t II Cn J
178 4 adantr φ r 0 1 P B
179 5 adantr φ r 0 1 F P = 0 G 0
180 simpr φ r 0 1 r 0 1
181 168 a1i φ r 0 1 0 0 1
182 1 176 177 178 179 6 7 46 180 181 cvmlift2lem10 φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C
183 df-3an r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C
184 simprr φ r 0 1 u II v II r u 0 v 0 v
185 11 ad3antrrr φ r 0 1 u II v II r u 0 v K : 0 1 × 0 1 B
186 185 ffnd φ r 0 1 u II v II r u 0 v K Fn 0 1 × 0 1
187 fnov K Fn 0 1 × 0 1 K = b 0 1 , w 0 1 b K w
188 186 187 sylib φ r 0 1 u II v II r u 0 v K = b 0 1 , w 0 1 b K w
189 188 reseq1d φ r 0 1 u II v II r u 0 v K u × 0 = b 0 1 , w 0 1 b K w u × 0
190 simplrl φ r 0 1 u II v II r u 0 v u II
191 elssuni u II u II
192 191 16 sseqtrrdi u II u 0 1
193 190 192 syl φ r 0 1 u II v II r u 0 v u 0 1
194 169 snssd φ 0 0 1
195 194 ad3antrrr φ r 0 1 u II v II r u 0 v 0 0 1
196 resmpo u 0 1 0 0 1 b 0 1 , w 0 1 b K w u × 0 = b u , w 0 b K w
197 193 195 196 syl2anc φ r 0 1 u II v II r u 0 v b 0 1 , w 0 1 b K w u × 0 = b u , w 0 b K w
198 193 sselda φ r 0 1 u II v II r u 0 v b u b 0 1
199 simplll φ r 0 1 u II v II r u 0 v φ
200 1 2 3 4 5 6 7 cvmlift2lem8 φ b 0 1 b K 0 = H b
201 199 200 sylan φ r 0 1 u II v II r u 0 v b 0 1 b K 0 = H b
202 198 201 syldan φ r 0 1 u II v II r u 0 v b u b K 0 = H b
203 elsni w 0 w = 0
204 203 oveq2d w 0 b K w = b K 0
205 204 eqeq1d w 0 b K w = H b b K 0 = H b
206 202 205 syl5ibrcom φ r 0 1 u II v II r u 0 v b u w 0 b K w = H b
207 206 3impia φ r 0 1 u II v II r u 0 v b u w 0 b K w = H b
208 207 mpoeq3dva φ r 0 1 u II v II r u 0 v b u , w 0 b K w = b u , w 0 H b
209 189 197 208 3eqtrd φ r 0 1 u II v II r u 0 v K u × 0 = b u , w 0 H b
210 eqid II 𝑡 u = II 𝑡 u
211 iitopon II TopOn 0 1
212 211 a1i φ r 0 1 u II v II r u 0 v II TopOn 0 1
213 eqid II 𝑡 0 = II 𝑡 0
214 212 212 cnmpt1st φ r 0 1 u II v II r u 0 v b 0 1 , w 0 1 b II × t II Cn II
215 1 2 3 4 5 6 cvmlift2lem2 φ H II Cn C F H = z 0 1 z G 0 H 0 = P
216 215 simp1d φ H II Cn C
217 199 216 syl φ r 0 1 u II v II r u 0 v H II Cn C
218 212 212 214 217 cnmpt21f φ r 0 1 u II v II r u 0 v b 0 1 , w 0 1 H b II × t II Cn C
219 210 212 193 213 212 195 218 cnmpt2res φ r 0 1 u II v II r u 0 v b u , w 0 H b II 𝑡 u × t II 𝑡 0 Cn C
220 vex u V
221 snex 0 V
222 txrest II Top II Top u V 0 V II × t II 𝑡 u × 0 = II 𝑡 u × t II 𝑡 0
223 22 22 220 221 222 mp4an II × t II 𝑡 u × 0 = II 𝑡 u × t II 𝑡 0
224 223 oveq1i II × t II 𝑡 u × 0 Cn C = II 𝑡 u × t II 𝑡 0 Cn C
225 219 224 eleqtrrdi φ r 0 1 u II v II r u 0 v b u , w 0 H b II × t II 𝑡 u × 0 Cn C
226 209 225 eqeltrd φ r 0 1 u II v II r u 0 v K u × 0 II × t II 𝑡 u × 0 Cn C
227 sneq w = 0 w = 0
228 227 xpeq2d w = 0 u × w = u × 0
229 228 reseq2d w = 0 K u × w = K u × 0
230 228 oveq2d w = 0 II × t II 𝑡 u × w = II × t II 𝑡 u × 0
231 230 oveq1d w = 0 II × t II 𝑡 u × w Cn C = II × t II 𝑡 u × 0 Cn C
232 229 231 eleq12d w = 0 K u × w II × t II 𝑡 u × w Cn C K u × 0 II × t II 𝑡 u × 0 Cn C
233 232 rspcev 0 v K u × 0 II × t II 𝑡 u × 0 Cn C w v K u × w II × t II 𝑡 u × w Cn C
234 184 226 233 syl2anc φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C
235 opelxpi r u 0 v r 0 u × v
236 235 adantl φ r 0 1 u II v II r u 0 v r 0 u × v
237 simplrr φ r 0 1 u II v II r u 0 v v II
238 237 145 syl φ r 0 1 u II v II r u 0 v v 0 1
239 xpss12 u 0 1 v 0 1 u × v 0 1 × 0 1
240 193 238 239 syl2anc φ r 0 1 u II v II r u 0 v u × v 0 1 × 0 1
241 38 restuni II × t II Top u × v 0 1 × 0 1 u × v = II × t II 𝑡 u × v
242 24 240 241 sylancr φ r 0 1 u II v II r u 0 v u × v = II × t II 𝑡 u × v
243 236 242 eleqtrd φ r 0 1 u II v II r u 0 v r 0 II × t II 𝑡 u × v
244 eqid II × t II 𝑡 u × v = II × t II 𝑡 u × v
245 244 cncnpi K u × v II × t II 𝑡 u × v Cn C r 0 II × t II 𝑡 u × v K u × v II × t II 𝑡 u × v CnP C r 0
246 245 expcom r 0 II × t II 𝑡 u × v K u × v II × t II 𝑡 u × v Cn C K u × v II × t II 𝑡 u × v CnP C r 0
247 243 246 syl φ r 0 1 u II v II r u 0 v K u × v II × t II 𝑡 u × v Cn C K u × v II × t II 𝑡 u × v CnP C r 0
248 24 a1i φ r 0 1 u II v II r u 0 v II × t II Top
249 22 a1i φ r 0 1 u II v II r u 0 v II Top
250 249 249 190 237 55 syl22anc φ r 0 1 u II v II r u 0 v u × v II × t II
251 isopn3i II × t II Top u × v II × t II int II × t II u × v = u × v
252 24 250 251 sylancr φ r 0 1 u II v II r u 0 v int II × t II u × v = u × v
253 236 252 eleqtrrd φ r 0 1 u II v II r u 0 v r 0 int II × t II u × v
254 38 1 cnprest II × t II Top u × v 0 1 × 0 1 r 0 int II × t II u × v K : 0 1 × 0 1 B K II × t II CnP C r 0 K u × v II × t II 𝑡 u × v CnP C r 0
255 248 240 253 185 254 syl22anc φ r 0 1 u II v II r u 0 v K II × t II CnP C r 0 K u × v II × t II 𝑡 u × v CnP C r 0
256 247 255 sylibrd φ r 0 1 u II v II r u 0 v K u × v II × t II 𝑡 u × v Cn C K II × t II CnP C r 0
257 234 256 embantd φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C K II × t II CnP C r 0
258 257 expimpd φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C K II × t II CnP C r 0
259 183 258 syl5bi φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C K II × t II CnP C r 0
260 259 rexlimdvva φ r 0 1 u II v II r u 0 v w v K u × w II × t II 𝑡 u × w Cn C K u × v II × t II 𝑡 u × v Cn C K II × t II CnP C r 0
261 182 260 mpd φ r 0 1 K II × t II CnP C r 0
262 fveq2 z = r 0 II × t II CnP C z = II × t II CnP C r 0
263 262 eleq2d z = r 0 K II × t II CnP C z K II × t II CnP C r 0
264 263 8 elrab2 r 0 M r 0 0 1 × 0 1 K II × t II CnP C r 0
265 175 261 264 sylanbrc φ r 0 1 r 0 M
266 elsni a 0 a = 0
267 266 opeq2d a 0 r a = r 0
268 267 eleq1d a 0 r a M r 0 M
269 265 268 syl5ibrcom φ r 0 1 a 0 r a M
270 269 expimpd φ r 0 1 a 0 r a M
271 172 270 syl5bi φ r a 0 1 × 0 r a M
272 171 271 relssdv φ 0 1 × 0 M
273 sneq a = 0 a = 0
274 273 xpeq2d a = 0 0 1 × a = 0 1 × 0
275 274 sseq1d a = 0 0 1 × a M 0 1 × 0 M
276 275 9 elrab2 0 A 0 0 1 0 1 × 0 M
277 169 272 276 sylanbrc φ 0 A
278 277 ne0d φ A
279 inss2 II Clsd II Clsd II
280 279 166 sseldi φ A Clsd II
281 16 18 167 278 280 connclo φ A = 0 1
282 281 9 eqtr3di φ 0 1 = a 0 1 | 0 1 × a M
283 rabid2 0 1 = a 0 1 | 0 1 × a M a 0 1 0 1 × a M
284 282 283 sylib φ a 0 1 0 1 × a M
285 iunss a 0 1 0 1 × a M a 0 1 0 1 × a M
286 284 285 sylibr φ a 0 1 0 1 × a M
287 15 286 eqsstrid φ 0 1 × 0 1 M
288 287 8 sseqtrdi φ 0 1 × 0 1 z 0 1 × 0 1 | K II × t II CnP C z
289 ssrab 0 1 × 0 1 z 0 1 × 0 1 | K II × t II CnP C z 0 1 × 0 1 0 1 × 0 1 z 0 1 × 0 1 K II × t II CnP C z
290 289 simprbi 0 1 × 0 1 z 0 1 × 0 1 | K II × t II CnP C z z 0 1 × 0 1 K II × t II CnP C z
291 288 290 syl φ z 0 1 × 0 1 K II × t II CnP C z
292 txtopon II TopOn 0 1 II TopOn 0 1 II × t II TopOn 0 1 × 0 1
293 211 211 292 mp2an II × t II TopOn 0 1 × 0 1
294 cvmtop1 F C CovMap J C Top
295 2 294 syl φ C Top
296 1 toptopon C Top C TopOn B
297 295 296 sylib φ C TopOn B
298 cncnp II × t II TopOn 0 1 × 0 1 C TopOn B K II × t II Cn C K : 0 1 × 0 1 B z 0 1 × 0 1 K II × t II CnP C z
299 293 297 298 sylancr φ K II × t II Cn C K : 0 1 × 0 1 B z 0 1 × 0 1 K II × t II CnP C z
300 11 291 299 mpbir2and φ K II × t II Cn C