Step | Hyp | Ref
| Expression |
1 | | cvmlift2.b |
. 2
|
2 | | iitop 22683 |
. . 3
|
3 | | iiuni 22684 |
. . 3
|
4 | 2, 2, 3, 3 | txunii 21396 |
. 2
|
5 | | cvmlift2lem10.s |
. 2
↾t
↾t |
6 | | cvmlift2.f |
. 2
CovMap |
7 | | cvmlift2.g |
. . 3
|
8 | | cvmlift2.p |
. . 3
|
9 | | cvmlift2.i |
. . 3
|
10 | | cvmlift2.h |
. . 3
|
11 | | cvmlift2.k |
. . 3
|
12 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem5 31289 |
. 2
|
13 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem7 31291 |
. . 3
|
14 | 13, 7 | eqeltrd 2701 |
. 2
|
15 | 2, 2 | txtopi 21393 |
. . 3
|
16 | 15 | a1i 11 |
. 2
|
17 | | cvmlift2lem9.3 |
. . . . 5
|
18 | | elssuni 4467 |
. . . . . 6
|
19 | 18, 3 | syl6sseqr 3652 |
. . . . 5
|
20 | 17, 19 | syl 17 |
. . . 4
|
21 | | cvmlift2lem9.7 |
. . . 4
|
22 | 20, 21 | sseldd 3604 |
. . 3
|
23 | | cvmlift2lem9.4 |
. . . . 5
|
24 | | elssuni 4467 |
. . . . . 6
|
25 | 24, 3 | syl6sseqr 3652 |
. . . . 5
|
26 | 23, 25 | syl 17 |
. . . 4
|
27 | | cvmlift2lem9.8 |
. . . 4
|
28 | 26, 27 | sseldd 3604 |
. . 3
|
29 | | opelxpi 5148 |
. . 3
|
30 | 22, 28, 29 | syl2anc 693 |
. 2
|
31 | | cvmlift2lem9.2 |
. 2
|
32 | 12, 22, 28 | fovrnd 6806 |
. . . 4
|
33 | | fvco3 6275 |
. . . . . . . 8
|
34 | 12, 30, 33 | syl2anc 693 |
. . . . . . 7
|
35 | 13 | fveq1d 6193 |
. . . . . . 7
|
36 | 34, 35 | eqtr3d 2658 |
. . . . . 6
|
37 | | df-ov 6653 |
. . . . . . 7
|
38 | 37 | fveq2i 6194 |
. . . . . 6
|
39 | | df-ov 6653 |
. . . . . 6
|
40 | 36, 38, 39 | 3eqtr4g 2681 |
. . . . 5
|
41 | | cvmlift2lem9.1 |
. . . . 5
|
42 | 40, 41 | eqeltrd 2701 |
. . . 4
|
43 | | cvmlift2lem9.w |
. . . . 5
|
44 | 5, 1, 43 | cvmsiota 31259 |
. . . 4
CovMap
|
45 | 6, 31, 32, 42, 44 | syl13anc 1328 |
. . 3
|
46 | 37 | eleq1i 2692 |
. . . 4
|
47 | 46 | anbi2i 730 |
. . 3
|
48 | 45, 47 | sylib 208 |
. 2
|
49 | | xpss12 5225 |
. . 3
|
50 | 20, 26, 49 | syl2anc 693 |
. 2
|
51 | | snidg 4206 |
. . . . . . 7
|
52 | 51 | ad2antrl 764 |
. . . . . 6
|
53 | | simprr 796 |
. . . . . 6
|
54 | | ovres 6800 |
. . . . . 6
|
55 | 52, 53, 54 | syl2anc 693 |
. . . . 5
|
56 | | eqid 2622 |
. . . . . . . 8
↾t ↾t |
57 | 2 | a1i 11 |
. . . . . . . . . 10
|
58 | | snex 4908 |
. . . . . . . . . . 11
|
59 | 58 | a1i 11 |
. . . . . . . . . 10
|
60 | 23 | adantr 481 |
. . . . . . . . . 10
|
61 | | txrest 21434 |
. . . . . . . . . 10
↾t ↾t
↾t |
62 | 57, 57, 59, 60, 61 | syl22anc 1327 |
. . . . . . . . 9
↾t ↾t
↾t |
63 | | iitopon 22682 |
. . . . . . . . . . . 12
TopOn |
64 | 20 | sselda 3603 |
. . . . . . . . . . . . 13
|
65 | 64 | adantrr 753 |
. . . . . . . . . . . 12
|
66 | | restsn2 20975 |
. . . . . . . . . . . 12
TopOn ↾t |
67 | 63, 65, 66 | sylancr 695 |
. . . . . . . . . . 11
↾t |
68 | | pwsn 4428 |
. . . . . . . . . . . 12
|
69 | | indisconn 21221 |
. . . . . . . . . . . 12
Conn |
70 | 68, 69 | eqeltri 2697 |
. . . . . . . . . . 11
Conn |
71 | 67, 70 | syl6eqel 2709 |
. . . . . . . . . 10
↾t Conn |
72 | | cvmlift2lem9.6 |
. . . . . . . . . . 11
↾t Conn |
73 | 72 | adantr 481 |
. . . . . . . . . 10
↾t Conn |
74 | | txconn 21492 |
. . . . . . . . . 10
↾t Conn
↾t
Conn
↾t ↾t Conn |
75 | 71, 73, 74 | syl2anc 693 |
. . . . . . . . 9
↾t ↾t Conn |
76 | 62, 75 | eqeltrd 2701 |
. . . . . . . 8
↾t Conn |
77 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem6 31290 |
. . . . . . . . . . . 12
↾t |
78 | 65, 77 | syldan 487 |
. . . . . . . . . . 11
↾t |
79 | 26 | adantr 481 |
. . . . . . . . . . . . 13
|
80 | | xpss2 5229 |
. . . . . . . . . . . . 13
|
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
|
82 | 65 | snssd 4340 |
. . . . . . . . . . . . . 14
|
83 | | xpss1 5228 |
. . . . . . . . . . . . . 14
|
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
|
85 | 4 | restuni 20966 |
. . . . . . . . . . . . 13
↾t |
86 | 15, 84, 85 | sylancr 695 |
. . . . . . . . . . . 12
↾t |
87 | 81, 86 | sseqtrd 3641 |
. . . . . . . . . . 11
↾t |
88 | | eqid 2622 |
. . . . . . . . . . . 12
↾t ↾t |
89 | 88 | cnrest 21089 |
. . . . . . . . . . 11
↾t
↾t
↾t ↾t |
90 | 78, 87, 89 | syl2anc 693 |
. . . . . . . . . 10
↾t ↾t |
91 | 81 | resabs1d 5428 |
. . . . . . . . . 10
|
92 | 15 | a1i 11 |
. . . . . . . . . . . 12
|
93 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
94 | 58, 93 | xpex 6962 |
. . . . . . . . . . . . 13
|
95 | 94 | a1i 11 |
. . . . . . . . . . . 12
|
96 | | restabs 20969 |
. . . . . . . . . . . 12
↾t ↾t ↾t |
97 | 92, 81, 95, 96 | syl3anc 1326 |
. . . . . . . . . . 11
↾t
↾t ↾t |
98 | 97 | oveq1d 6665 |
. . . . . . . . . 10
↾t ↾t ↾t |
99 | 90, 91, 98 | 3eltr3d 2715 |
. . . . . . . . 9
↾t |
100 | | cvmtop1 31242 |
. . . . . . . . . . . . 13
CovMap
|
101 | 6, 100 | syl 17 |
. . . . . . . . . . . 12
|
102 | 101 | adantr 481 |
. . . . . . . . . . 11
|
103 | 1 | toptopon 20722 |
. . . . . . . . . . 11
TopOn |
104 | 102, 103 | sylib 208 |
. . . . . . . . . 10
TopOn |
105 | | df-ima 5127 |
. . . . . . . . . . 11
|
106 | | simprl 794 |
. . . . . . . . . . . . . 14
|
107 | 106 | snssd 4340 |
. . . . . . . . . . . . 13
|
108 | | xpss1 5228 |
. . . . . . . . . . . . 13
|
109 | | imass2 5501 |
. . . . . . . . . . . . 13
|
110 | 107, 108,
109 | 3syl 18 |
. . . . . . . . . . . 12
|
111 | | cvmlift2lem9.9 |
. . . . . . . . . . . . . . 15
|
112 | | imaco 5640 |
. . . . . . . . . . . . . . . 16
|
113 | | cnvco 5308 |
. . . . . . . . . . . . . . . . . 18
|
114 | 13 | cnveqd 5298 |
. . . . . . . . . . . . . . . . . 18
|
115 | 113, 114 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | imaeq1d 5465 |
. . . . . . . . . . . . . . . 16
|
117 | 112, 116 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
118 | 111, 117 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
|
119 | | ffun 6048 |
. . . . . . . . . . . . . . . 16
|
120 | 12, 119 | syl 17 |
. . . . . . . . . . . . . . 15
|
121 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
|
122 | 12, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
|
123 | 50, 122 | sseqtr4d 3642 |
. . . . . . . . . . . . . . 15
|
124 | | funimass3 6333 |
. . . . . . . . . . . . . . 15
|
125 | 120, 123,
124 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
126 | 118, 125 | mpbird 247 |
. . . . . . . . . . . . 13
|
127 | 126 | adantr 481 |
. . . . . . . . . . . 12
|
128 | 110, 127 | sstrd 3613 |
. . . . . . . . . . 11
|
129 | 105, 128 | syl5eqssr 3650 |
. . . . . . . . . 10
|
130 | | cnvimass 5485 |
. . . . . . . . . . . 12
|
131 | | cvmcn 31244 |
. . . . . . . . . . . . . 14
CovMap
|
132 | 6, 131 | syl 17 |
. . . . . . . . . . . . 13
|
133 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
134 | 1, 133 | cnf 21050 |
. . . . . . . . . . . . 13
|
135 | | fdm 6051 |
. . . . . . . . . . . . 13
|
136 | 132, 134,
135 | 3syl 18 |
. . . . . . . . . . . 12
|
137 | 130, 136 | syl5sseq 3653 |
. . . . . . . . . . 11
|
138 | 137 | adantr 481 |
. . . . . . . . . 10
|
139 | | cnrest2 21090 |
. . . . . . . . . 10
TopOn
↾t
↾t ↾t |
140 | 104, 129,
138, 139 | syl3anc 1326 |
. . . . . . . . 9
↾t ↾t ↾t |
141 | 99, 140 | mpbid 222 |
. . . . . . . 8
↾t ↾t |
142 | 5 | cvmsss 31249 |
. . . . . . . . . . . 12
|
143 | 31, 142 | syl 17 |
. . . . . . . . . . 11
|
144 | 45 | simpld 475 |
. . . . . . . . . . 11
|
145 | 143, 144 | sseldd 3604 |
. . . . . . . . . 10
|
146 | | elssuni 4467 |
. . . . . . . . . . . 12
|
147 | 144, 146 | syl 17 |
. . . . . . . . . . 11
|
148 | 5 | cvmsuni 31251 |
. . . . . . . . . . . 12
|
149 | 31, 148 | syl 17 |
. . . . . . . . . . 11
|
150 | 147, 149 | sseqtrd 3641 |
. . . . . . . . . 10
|
151 | 5 | cvmsrcl 31246 |
. . . . . . . . . . . . 13
|
152 | 31, 151 | syl 17 |
. . . . . . . . . . . 12
|
153 | | cnima 21069 |
. . . . . . . . . . . 12
|
154 | 132, 152,
153 | syl2anc 693 |
. . . . . . . . . . 11
|
155 | | restopn2 20981 |
. . . . . . . . . . 11
↾t
|
156 | 101, 154,
155 | syl2anc 693 |
. . . . . . . . . 10
↾t
|
157 | 145, 150,
156 | mpbir2and 957 |
. . . . . . . . 9
↾t |
158 | 157 | adantr 481 |
. . . . . . . 8
↾t |
159 | 5 | cvmscld 31255 |
. . . . . . . . . 10
CovMap
↾t |
160 | 6, 31, 144, 159 | syl3anc 1326 |
. . . . . . . . 9
↾t |
161 | 160 | adantr 481 |
. . . . . . . 8
↾t |
162 | | cvmlift2lem9.10 |
. . . . . . . . . . 11
|
163 | 162 | adantr 481 |
. . . . . . . . . 10
|
164 | | opelxpi 5148 |
. . . . . . . . . 10
|
165 | 52, 163, 164 | syl2anc 693 |
. . . . . . . . 9
|
166 | 81, 84 | sstrd 3613 |
. . . . . . . . . 10
|
167 | 4 | restuni 20966 |
. . . . . . . . . 10
↾t |
168 | 15, 166, 167 | sylancr 695 |
. . . . . . . . 9
↾t |
169 | 165, 168 | eleqtrd 2703 |
. . . . . . . 8
↾t |
170 | | df-ov 6653 |
. . . . . . . . . 10
|
171 | | ovres 6800 |
. . . . . . . . . . . 12
|
172 | 52, 163, 171 | syl2anc 693 |
. . . . . . . . . . 11
|
173 | | snidg 4206 |
. . . . . . . . . . . . . 14
|
174 | 162, 173 | syl 17 |
. . . . . . . . . . . . 13
|
175 | 174 | adantr 481 |
. . . . . . . . . . . 12
|
176 | | ovres 6800 |
. . . . . . . . . . . 12
|
177 | 106, 175,
176 | syl2anc 693 |
. . . . . . . . . . 11
|
178 | 172, 177 | eqtr4d 2659 |
. . . . . . . . . 10
|
179 | 170, 178 | syl5eqr 2670 |
. . . . . . . . 9
|
180 | | eqid 2622 |
. . . . . . . . . . . . 13
↾t
↾t |
181 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
|
182 | | snex 4908 |
. . . . . . . . . . . . . . . 16
|
183 | 182 | a1i 11 |
. . . . . . . . . . . . . . 15
|
184 | | txrest 21434 |
. . . . . . . . . . . . . . 15
↾t
↾t ↾t |
185 | 181, 181,
17, 183, 184 | syl22anc 1327 |
. . . . . . . . . . . . . 14
↾t ↾t ↾t |
186 | | cvmlift2lem9.5 |
. . . . . . . . . . . . . . 15
↾t Conn |
187 | 26, 162 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
188 | | restsn2 20975 |
. . . . . . . . . . . . . . . . 17
TopOn ↾t |
189 | 63, 187, 188 | sylancr 695 |
. . . . . . . . . . . . . . . 16
↾t |
190 | | pwsn 4428 |
. . . . . . . . . . . . . . . . 17
|
191 | | indisconn 21221 |
. . . . . . . . . . . . . . . . 17
Conn |
192 | 190, 191 | eqeltri 2697 |
. . . . . . . . . . . . . . . 16
Conn |
193 | 189, 192 | syl6eqel 2709 |
. . . . . . . . . . . . . . 15
↾t Conn |
194 | | txconn 21492 |
. . . . . . . . . . . . . . 15
↾t Conn
↾t Conn
↾t ↾t Conn |
195 | 186, 193,
194 | syl2anc 693 |
. . . . . . . . . . . . . 14
↾t ↾t Conn |
196 | 185, 195 | eqeltrd 2701 |
. . . . . . . . . . . . 13
↾t Conn |
197 | | cvmlift2lem9.11 |
. . . . . . . . . . . . . 14
↾t |
198 | 101, 103 | sylib 208 |
. . . . . . . . . . . . . . 15
TopOn |
199 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
|
200 | 162 | snssd 4340 |
. . . . . . . . . . . . . . . . . 18
|
201 | | xpss2 5229 |
. . . . . . . . . . . . . . . . . 18
|
202 | | imass2 5501 |
. . . . . . . . . . . . . . . . . 18
|
203 | 200, 201,
202 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
204 | 203, 126 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
205 | 199, 204 | syl5eqssr 3650 |
. . . . . . . . . . . . . . 15
|
206 | | cnrest2 21090 |
. . . . . . . . . . . . . . 15
TopOn
↾t
↾t ↾t |
207 | 198, 205,
137, 206 | syl3anc 1326 |
. . . . . . . . . . . . . 14
↾t
↾t ↾t |
208 | 197, 207 | mpbid 222 |
. . . . . . . . . . . . 13
↾t ↾t |
209 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
|
210 | 21, 174, 209 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
211 | 187 | snssd 4340 |
. . . . . . . . . . . . . . . 16
|
212 | | xpss12 5225 |
. . . . . . . . . . . . . . . 16
|
213 | 20, 211, 212 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
214 | 4 | restuni 20966 |
. . . . . . . . . . . . . . 15
↾t |
215 | 15, 213, 214 | sylancr 695 |
. . . . . . . . . . . . . 14
↾t |
216 | 210, 215 | eleqtrd 2703 |
. . . . . . . . . . . . 13
↾t |
217 | | df-ov 6653 |
. . . . . . . . . . . . . . 15
|
218 | | ovres 6800 |
. . . . . . . . . . . . . . . . 17
|
219 | 21, 174, 218 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
220 | | snidg 4206 |
. . . . . . . . . . . . . . . . . 18
|
221 | 21, 220 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
222 | | ovres 6800 |
. . . . . . . . . . . . . . . . 17
|
223 | 221, 162,
222 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
224 | 219, 223 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
|
225 | 217, 224 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
|
226 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
↾t ↾t |
227 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . 20
|
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
229 | | txrest 21434 |
. . . . . . . . . . . . . . . . . . 19
↾t ↾t ↾t |
230 | 181, 181,
228, 23, 229 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
↾t ↾t ↾t |
231 | | restsn2 20975 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn ↾t |
232 | 63, 22, 231 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
↾t |
233 | | pwsn 4428 |
. . . . . . . . . . . . . . . . . . . . 21
|
234 | | indisconn 21221 |
. . . . . . . . . . . . . . . . . . . . 21
Conn |
235 | 233, 234 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . 20
Conn |
236 | 232, 235 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . 19
↾t Conn |
237 | | txconn 21492 |
. . . . . . . . . . . . . . . . . . 19
↾t Conn
↾t
Conn
↾t ↾t Conn |
238 | 236, 72, 237 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
↾t ↾t Conn |
239 | 230, 238 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
↾t Conn |
240 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem6 31290 |
. . . . . . . . . . . . . . . . . . . . 21
↾t |
241 | 22, 240 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . 20
↾t |
242 | | xpss2 5229 |
. . . . . . . . . . . . . . . . . . . . . 22
|
243 | 23, 25, 242 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
|
244 | 22 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
245 | | xpss1 5228 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
247 | 4 | restuni 20966 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t |
248 | 15, 246, 247 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
↾t |
249 | 243, 248 | sseqtrd 3641 |
. . . . . . . . . . . . . . . . . . . 20
↾t |
250 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
↾t ↾t |
251 | 250 | cnrest 21089 |
. . . . . . . . . . . . . . . . . . . 20
↾t ↾t
↾t
↾t |
252 | 241, 249,
251 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t |
253 | 243 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . . 19
|
254 | 227, 93 | xpex 6962 |
. . . . . . . . . . . . . . . . . . . . . 22
|
255 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
256 | | restabs 20969 |
. . . . . . . . . . . . . . . . . . . . 21
↾t
↾t ↾t |
257 | 16, 243, 255, 256 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
↾t
↾t ↾t |
258 | 257 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t ↾t |
259 | 252, 253,
258 | 3eltr3d 2715 |
. . . . . . . . . . . . . . . . . 18
↾t |
260 | | df-ima 5127 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | 21 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . 22
|
262 | | xpss1 5228 |
. . . . . . . . . . . . . . . . . . . . . 22
|
263 | | imass2 5501 |
. . . . . . . . . . . . . . . . . . . . . 22
|
264 | 261, 262,
263 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
|
265 | 264, 126 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . 20
|
266 | 260, 265 | syl5eqssr 3650 |
. . . . . . . . . . . . . . . . . . 19
|
267 | | cnrest2 21090 |
. . . . . . . . . . . . . . . . . . 19
TopOn
↾t ↾t ↾t |
268 | 198, 266,
137, 267 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
↾t ↾t ↾t |
269 | 259, 268 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
↾t ↾t |
270 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . 19
|
271 | 221, 27, 270 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
272 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
273 | 272, 50 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . 19
|
274 | 4 | restuni 20966 |
. . . . . . . . . . . . . . . . . . 19
↾t |
275 | 15, 273, 274 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
↾t |
276 | 271, 275 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . 17
↾t |
277 | | df-ov 6653 |
. . . . . . . . . . . . . . . . . . 19
|
278 | | ovres 6800 |
. . . . . . . . . . . . . . . . . . . 20
|
279 | 221, 27, 278 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
280 | 277, 279 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . 18
|
281 | 45 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
282 | 280, 281 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
283 | 226, 239,
269, 157, 160, 276, 282 | conncn 21229 |
. . . . . . . . . . . . . . . 16
↾t |
284 | 275 | feq2d 6031 |
. . . . . . . . . . . . . . . 16
↾t |
285 | 283, 284 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
286 | 285, 221,
162 | fovrnd 6806 |
. . . . . . . . . . . . . 14
|
287 | 225, 286 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
288 | 180, 196,
208, 157, 160, 216, 287 | conncn 21229 |
. . . . . . . . . . . 12
↾t |
289 | 215 | feq2d 6031 |
. . . . . . . . . . . 12
↾t |
290 | 288, 289 | mpbird 247 |
. . . . . . . . . . 11
|
291 | 290 | adantr 481 |
. . . . . . . . . 10
|
292 | 291, 106,
175 | fovrnd 6806 |
. . . . . . . . 9
|
293 | 179, 292 | eqeltrd 2701 |
. . . . . . . 8
|
294 | 56, 76, 141, 158, 161, 169, 293 | conncn 21229 |
. . . . . . 7
↾t |
295 | 168 | feq2d 6031 |
. . . . . . 7
↾t |
296 | 294, 295 | mpbird 247 |
. . . . . 6
|
297 | 296, 52, 53 | fovrnd 6806 |
. . . . 5
|
298 | 55, 297 | eqeltrrd 2702 |
. . . 4
|
299 | 298 | ralrimivva 2971 |
. . 3
|
300 | | funimassov 6811 |
. . . 4
|
301 | 120, 123,
300 | syl2anc 693 |
. . 3
|
302 | 299, 301 | mpbird 247 |
. 2
|
303 | 1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 302 | cvmlift2lem9a 31285 |
1
↾t |