Step | Hyp | Ref
| Expression |
1 | | cvmlift2.b |
. . 3
|
2 | | cvmlift2.f |
. . 3
CovMap |
3 | | cvmlift2.g |
. . 3
|
4 | | cvmlift2.p |
. . 3
|
5 | | cvmlift2.i |
. . 3
|
6 | | cvmlift2.h |
. . 3
|
7 | | cvmlift2.k |
. . 3
|
8 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem5 31289 |
. 2
|
9 | | iunid 4575 |
. . . . . . 7
|
10 | 9 | xpeq2i 5136 |
. . . . . 6
|
11 | | xpiundi 5173 |
. . . . . 6
|
12 | 10, 11 | eqtr3i 2646 |
. . . . 5
|
13 | | cvmlift2.a |
. . . . . . . 8
|
14 | | iiuni 22684 |
. . . . . . . . 9
|
15 | | iiconn 22690 |
. . . . . . . . . 10
Conn |
16 | 15 | a1i 11 |
. . . . . . . . 9
Conn |
17 | | inss1 3833 |
. . . . . . . . . 10
|
18 | | iicmp 22689 |
. . . . . . . . . . . . . . 15
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
|
20 | | iitop 22683 |
. . . . . . . . . . . . . . 15
|
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
|
22 | 20, 20 | txtopi 21393 |
. . . . . . . . . . . . . . . 16
|
23 | 14 | neiss2 20905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
24 | 20, 23 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
25 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
26 | 25 | snss 4316 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
27 | 24, 26 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
|
28 | 27 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
|
29 | 28 | rexlimiv 3027 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
31 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 30, 31 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | ssopab2i 5003 |
. . . . . . . . . . . . . . . . 17
|
34 | | cvmlift2.s |
. . . . . . . . . . . . . . . . 17
|
35 | | df-xp 5120 |
. . . . . . . . . . . . . . . . 17
|
36 | 33, 34, 35 | 3sstr4i 3644 |
. . . . . . . . . . . . . . . 16
|
37 | 20, 20, 14, 14 | txunii 21396 |
. . . . . . . . . . . . . . . . 17
|
38 | 37 | ntropn 20853 |
. . . . . . . . . . . . . . . 16
|
39 | 22, 36, 38 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
|
41 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
CovMap |
42 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
↾t ↾t
↾t
↾t |
46 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 1, 41, 42, 43, 44, 6, 7, 45, 46, 47 | cvmlift2lem10 31294 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t |
49 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
50 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
51 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t
|
52 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t
|
53 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t
|
54 | | txopn 21405 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
55 | 51, 51, 52, 53, 54 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
56 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
57 | | elunii 4441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
58 | 57, 14 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
59 | 56, 53, 58 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
↾t
↾t |
60 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
↾t
↾t |
61 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
↾t
↾t
|
62 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
↾t
↾t |
63 | | opnneip 20923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
64 | 60, 61, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
↾t
↾t
|
65 | 41 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t
CovMap |
66 | 42 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t
|
67 | 43 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t
|
68 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t |
69 | | cvmlift2.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
70 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t |
71 | | simplr2 1104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t |
72 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t |
73 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
74 | 73 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
75 | 74 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
76 | 74 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
↾t
↾t |
77 | 76 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
↾t
↾t |
78 | 75, 77 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
↾t
↾t |
79 | 78 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
↾t
↾t |
80 | | simplr3 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
↾t
↾t
↾t
↾t |
81 | 79, 80 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
↾t
↾t
↾t
↾t |
82 | 1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81 | cvmlift2lem11 31295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
↾t
↾t |
83 | 1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81 | cvmlift2lem11 31295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
↾t
↾t |
84 | 82, 83 | impbid 202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
↾t
↾t
|
85 | | rspe 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
86 | 64, 84, 85 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
↾t
↾t
|
87 | 59, 86 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
↾t
↾t |
88 | 87 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t
↾t
|
89 | 88 | alrimivv 1856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t
|
90 | | df-xp 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
91 | 90, 34 | sseq12i 3631 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
92 | | ssopab2b 5002 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
93 | 91, 92 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 89, 93 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
95 | 37 | ssntr 20862 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
96 | 49, 50, 55, 94, 95 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
↾t
|
97 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
98 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
|
99 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 97, 98, 99 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
↾t
|
101 | 96, 100 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
↾t
↾t
|
102 | 101 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
↾t
↾t
|
103 | 102 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t
|
104 | 48, 103 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
|
105 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
106 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 106 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 105, 107 | ralsn 4222 |
. . . . . . . . . . . . . . . . . 18
|
109 | 104, 108 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | anassrs 680 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
|
112 | | dfss3 3592 |
. . . . . . . . . . . . . . . 16
|
113 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
114 | 113 | ralxp 5263 |
. . . . . . . . . . . . . . . 16
|
115 | 112, 114 | bitri 264 |
. . . . . . . . . . . . . . 15
|
116 | 111, 115 | sylibr 224 |
. . . . . . . . . . . . . 14
|
117 | | simpr 477 |
. . . . . . . . . . . . . 14
|
118 | 14, 14, 19, 21, 40, 116, 117 | txtube 21443 |
. . . . . . . . . . . . 13
|
119 | 37 | ntrss2 20861 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 22, 36, 119 | mp2an 708 |
. . . . . . . . . . . . . . . . . 18
|
121 | | sstr 3611 |
. . . . . . . . . . . . . . . . . 18
|
122 | 120, 121 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
|
123 | | df-xp 5120 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 123, 34 | sseq12i 3631 |
. . . . . . . . . . . . . . . . . 18
|
125 | | ssopab2b 5002 |
. . . . . . . . . . . . . . . . . . 19
|
126 | | r2al 2939 |
. . . . . . . . . . . . . . . . . . 19
|
127 | | ralcom 3098 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 125, 126,
127 | 3bitr2i 288 |
. . . . . . . . . . . . . . . . . 18
|
129 | 124, 128 | bitri 264 |
. . . . . . . . . . . . . . . . 17
|
130 | 122, 129 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
131 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | 131 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . 19
|
133 | | cvmlift2lem1 31284 |
. . . . . . . . . . . . . . . . . . . 20
|
134 | | bicom 212 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
135 | 134 | rexbii 3041 |
. . . . . . . . . . . . . . . . . . . . . 22
|
136 | 135 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . 21
|
137 | | cvmlift2lem1 31284 |
. . . . . . . . . . . . . . . . . . . . 21
|
138 | 136, 137 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
|
139 | 133, 138 | impbid 202 |
. . . . . . . . . . . . . . . . . . 19
|
140 | 132, 139 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
141 | 13 | rabeq2i 3197 |
. . . . . . . . . . . . . . . . . . . . 21
|
142 | 141 | baib 944 |
. . . . . . . . . . . . . . . . . . . 20
|
143 | 142 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . 19
|
144 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
145 | 144, 14 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . . . . . . 22
|
146 | 145 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
147 | 146 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
|
148 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
149 | 148 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | 149 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 150, 13 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 151 | baib 944 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
154 | 143, 153 | bibi12d 335 |
. . . . . . . . . . . . . . . . . 18
|
155 | 140, 154 | syl5ibr 236 |
. . . . . . . . . . . . . . . . 17
|
156 | 155 | ralimdva 2962 |
. . . . . . . . . . . . . . . 16
|
157 | 130, 156 | syl5 34 |
. . . . . . . . . . . . . . 15
|
158 | 157 | anim2d 589 |
. . . . . . . . . . . . . 14
|
159 | 158 | reximdva 3017 |
. . . . . . . . . . . . 13
|
160 | 118, 159 | mpd 15 |
. . . . . . . . . . . 12
|
161 | 160 | ralrimiva 2966 |
. . . . . . . . . . 11
|
162 | | ssrab2 3687 |
. . . . . . . . . . . . 13
|
163 | 13, 162 | eqsstri 3635 |
. . . . . . . . . . . 12
|
164 | 14 | isclo 20891 |
. . . . . . . . . . . 12
|
165 | 20, 163, 164 | mp2an 708 |
. . . . . . . . . . 11
|
166 | 161, 165 | sylibr 224 |
. . . . . . . . . 10
|
167 | 17, 166 | sseldi 3601 |
. . . . . . . . 9
|
168 | | 0elunit 12290 |
. . . . . . . . . . . 12
|
169 | 168 | a1i 11 |
. . . . . . . . . . 11
|
170 | | relxp 5227 |
. . . . . . . . . . . . 13
|
171 | 170 | a1i 11 |
. . . . . . . . . . . 12
|
172 | | opelxp 5146 |
. . . . . . . . . . . . 13
|
173 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
174 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . 17
|
175 | 173, 169,
174 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
|
176 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
CovMap |
177 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
178 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
179 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
180 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
181 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
182 | 1, 176, 177, 178, 179, 6, 7, 45, 180, 181 | cvmlift2lem10 31294 |
. . . . . . . . . . . . . . . . 17
↾t
↾t |
183 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t
↾t
↾t |
184 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
185 | 8 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
186 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
188 | | fnov 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
189 | 187, 188 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
190 | 189 | reseq1d 5395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
191 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
192 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
193 | 192, 14 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
194 | 191, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
195 | 169 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
196 | 195 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
197 | | resmpt2 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
198 | 194, 196,
197 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
199 | 194 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
200 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
201 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem8 31292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
202 | 200, 201 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
203 | 199, 202 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
204 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
205 | 204 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
206 | 205 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
207 | 203, 206 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
208 | 207 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
209 | 208 | mpt2eq3dva 6719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
210 | 190, 198,
209 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
211 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t ↾t |
212 | | iitopon 22682 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
TopOn |
213 | 212 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
TopOn |
214 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t
↾t |
215 | 213, 213 | cnmpt1st 21471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
216 | 1, 2, 3, 4, 5, 6 | cvmlift2lem2 31286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
217 | 216 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
218 | 200, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
219 | 213, 213,
215, 218 | cnmpt21f 21475 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
220 | 211, 213,
194, 214, 213, 196, 219 | cnmpt2res 21480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t ↾t |
221 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
222 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
223 | | txrest 21434 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
↾t
↾t ↾t |
224 | 20, 20, 221, 222, 223 | mp4an 709 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t ↾t ↾t |
225 | 224 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t ↾t |
226 | 220, 225 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t |
227 | 210, 226 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
|
228 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
229 | 228 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
230 | 229 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
231 | 229 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t
↾t |
232 | 231 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t |
233 | 230, 232 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t |
234 | 233 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
↾t |
235 | 184, 227,
234 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
↾t |
236 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
237 | 236 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
238 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
239 | 238, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
240 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
241 | 194, 239,
240 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
242 | 37 | restuni 20966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t
|
243 | 22, 241, 242 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t |
244 | 237, 243 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t |
245 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
↾t
↾t |
246 | 245 | cncnpi 21082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
↾t
↾t
↾t |
247 | 246 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t
↾t
↾t |
248 | 244, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
↾t |
249 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
250 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
251 | 250, 250,
191, 238, 54 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
252 | | isopn3i 20886 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
253 | 22, 251, 252 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
254 | 237, 253 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
255 | 37, 1 | cnprest 21093 |
. . . . . . . . . . . . . . . . . . . . . . 23
↾t |
256 | 249, 241,
254, 185, 255 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t |
257 | 248, 256 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . 21
↾t
|
258 | 235, 257 | embantd 59 |
. . . . . . . . . . . . . . . . . . . 20
↾t
↾t
|
259 | 258 | expimpd 629 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t
|
260 | 183, 259 | syl5bi 232 |
. . . . . . . . . . . . . . . . . 18
↾t
↾t
|
261 | 260 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . 17
↾t
↾t
|
262 | 182, 261 | mpd 15 |
. . . . . . . . . . . . . . . 16
|
263 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
264 | 263 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
|
265 | 264, 69 | elrab2 3366 |
. . . . . . . . . . . . . . . 16
|
266 | 175, 262,
265 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
267 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
|
268 | 267 | opeq2d 4409 |
. . . . . . . . . . . . . . . 16
|
269 | 268 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
270 | 266, 269 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
|
271 | 270 | expimpd 629 |
. . . . . . . . . . . . 13
|
272 | 172, 271 | syl5bi 232 |
. . . . . . . . . . . 12
|
273 | 171, 272 | relssdv 5212 |
. . . . . . . . . . 11
|
274 | | sneq 4187 |
. . . . . . . . . . . . . 14
|
275 | 274 | xpeq2d 5139 |
. . . . . . . . . . . . 13
|
276 | 275 | sseq1d 3632 |
. . . . . . . . . . . 12
|
277 | 276, 13 | elrab2 3366 |
. . . . . . . . . . 11
|
278 | 169, 273,
277 | sylanbrc 698 |
. . . . . . . . . 10
|
279 | | ne0i 3921 |
. . . . . . . . . 10
|
280 | 278, 279 | syl 17 |
. . . . . . . . 9
|
281 | | inss2 3834 |
. . . . . . . . . 10
|
282 | 281, 166 | sseldi 3601 |
. . . . . . . . 9
|
283 | 14, 16, 167, 280, 282 | connclo 21218 |
. . . . . . . 8
|
284 | 13, 283 | syl5reqr 2671 |
. . . . . . 7
|
285 | | rabid2 3118 |
. . . . . . 7
|
286 | 284, 285 | sylib 208 |
. . . . . 6
|
287 | | iunss 4561 |
. . . . . 6
|
288 | 286, 287 | sylibr 224 |
. . . . 5
|
289 | 12, 288 | syl5eqss 3649 |
. . . 4
|
290 | 289, 69 | syl6sseq 3651 |
. . 3
|
291 | | ssrab 3680 |
. . . 4
|
292 | 291 | simprbi 480 |
. . 3
|
293 | 290, 292 | syl 17 |
. 2
|
294 | | txtopon 21394 |
. . . 4
TopOn TopOn
TopOn |
295 | 212, 212,
294 | mp2an 708 |
. . 3
TopOn |
296 | | cvmtop1 31242 |
. . . . 5
CovMap
|
297 | 2, 296 | syl 17 |
. . . 4
|
298 | 1 | toptopon 20722 |
. . . 4
TopOn |
299 | 297, 298 | sylib 208 |
. . 3
TopOn |
300 | | cncnp 21084 |
. . 3
TopOn TopOn
|
301 | 295, 299,
300 | sylancr 695 |
. 2
|
302 | 8, 293, 301 | mpbir2and 957 |
1
|