Step | Hyp | Ref
| Expression |
1 | | prdsxms.i |
. . . 4
|
2 | | topnfn 16086 |
. . . . 5
|
3 | | prdsxms.r |
. . . . . . 7
|
4 | | ffn 6045 |
. . . . . . 7
|
5 | 3, 4 | syl 17 |
. . . . . 6
|
6 | | dffn2 6047 |
. . . . . 6
|
7 | 5, 6 | sylib 208 |
. . . . 5
|
8 | | fnfco 6069 |
. . . . 5
|
9 | 2, 7, 8 | sylancr 695 |
. . . 4
|
10 | | prdsxms.c |
. . . . 5
|
11 | 10 | ptval 21373 |
. . . 4
|
12 | 1, 9, 11 | syl2anc 693 |
. . 3
|
13 | | eldifsn 4317 |
. . . . . . . 8
|
14 | | prdsxms.y |
. . . . . . . . . . . 12
s |
15 | | prdsxms.s |
. . . . . . . . . . . 12
|
16 | | prdsxms.d |
. . . . . . . . . . . 12
|
17 | | prdsxms.b |
. . . . . . . . . . . 12
|
18 | 14, 15, 1, 16, 17, 3 | prdsxmslem1 22333 |
. . . . . . . . . . 11
|
19 | | blrn 22214 |
. . . . . . . . . . 11
|
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
|
21 | 18 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
22 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
23 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
24 | | xbln0 22219 |
. . . . . . . . . . . . . . . 16
|
25 | 21, 22, 23, 24 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
26 | 1 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
27 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . 18
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
29 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | rgenw 2924 |
. . . . . . . . . . . . . . . . . 18
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | fnmpt 6020 |
. . . . . . . . . . . . . . . . . 18
|
33 | 30, 32 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
|
34 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 34 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | | prdsxms.v |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | | prdsxms.e |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | 36, 37 | xmsxmet 22261 |
. . . . . . . . . . . . . . . . . . . . 21
|
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
s s |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
s s |
42 | 15 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
|
43 | 35 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . 22
|
44 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 34 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
s s |
47 | 14, 46 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
s |
48 | 47 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
s |
49 | 17, 48 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
s |
50 | 44, 49 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . 22
s |
51 | 40, 41, 42, 26, 43, 36, 50 | prdsbascl 16143 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 51 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | | simp2r 1088 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 55 | blopn 22305 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 39, 52, 54, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
58 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
60 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
61 | 60, 36 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
62 | 61 | sqxpeqd 5141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
63 | 59, 62 | reseq12d 5397 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | 63, 37 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 65, 66, 67 | oveq123d 6671 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 68, 31, 69 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
72 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | | prdsxms.k |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 72, 73 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 34, 74 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 73, 36, 37 | xmstopn 22256 |
. . . . . . . . . . . . . . . . . . . . 21
|
77 | 35, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 75, 77 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 57, 71, 78 | 3eltr4d 2716 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
81 | 34 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 81 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
s s |
83 | 14, 82 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
s |
84 | 83 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
s |
85 | 16, 84 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . 20
s |
86 | 85 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
s |
87 | 86 | oveqd 6667 |
. . . . . . . . . . . . . . . . . 18
s |
88 | 58 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . 19
s s |
90 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
s s |
91 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
s s |
92 | 83 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
s |
93 | 17, 92 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . 20
s |
94 | 44, 93 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
s |
95 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 89, 90, 36, 37, 91, 42, 26, 35, 39, 94, 53, 95 | prdsbl 22296 |
. . . . . . . . . . . . . . . . . 18
s
|
97 | 87, 96 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
98 | | fneq1 5979 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 99 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 100 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 98, 101 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 99, 70 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | ixpeq2dva 7923 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 104 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 102, 105 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 106 | spcegv 3294 |
. . . . . . . . . . . . . . . . . 18
|
108 | 107 | 3impib 1262 |
. . . . . . . . . . . . . . . . 17
|
109 | 28, 33, 80, 97, 108 | syl121anc 1331 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | 3expia 1267 |
. . . . . . . . . . . . . . 15
|
111 | 25, 110 | sylbid 230 |
. . . . . . . . . . . . . 14
|
112 | 111 | adantr 481 |
. . . . . . . . . . . . 13
|
113 | | simpr 477 |
. . . . . . . . . . . . . 14
|
114 | 113 | neeq1d 2853 |
. . . . . . . . . . . . 13
|
115 | | ral0 4076 |
. . . . . . . . . . . . . . . . . . 19
|
116 | | difeq2 3722 |
. . . . . . . . . . . . . . . . . . . . . 22
|
117 | | difid 3948 |
. . . . . . . . . . . . . . . . . . . . . 22
|
118 | 116, 117 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 119 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 1, 115, 120 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
122 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
123 | 122 | biantrud 528 |
. . . . . . . . . . . . . . . 16
|
124 | | df-3an 1039 |
. . . . . . . . . . . . . . . 16
|
125 | 123, 124 | syl6rbbr 279 |
. . . . . . . . . . . . . . 15
|
126 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
127 | 125, 126 | bi2anan9 917 |
. . . . . . . . . . . . . 14
|
128 | 127 | exbidv 1850 |
. . . . . . . . . . . . 13
|
129 | 112, 114,
128 | 3imtr4d 283 |
. . . . . . . . . . . 12
|
130 | 129 | ex 450 |
. . . . . . . . . . 11
|
131 | 130 | rexlimdvva 3038 |
. . . . . . . . . 10
|
132 | 20, 131 | sylbid 230 |
. . . . . . . . 9
|
133 | 132 | impd 447 |
. . . . . . . 8
|
134 | 13, 133 | syl5bi 232 |
. . . . . . 7
|
135 | 134 | alrimiv 1855 |
. . . . . 6
|
136 | | ssab 3672 |
. . . . . 6
|
137 | 135, 136 | sylibr 224 |
. . . . 5
|
138 | 137, 10 | syl6sseqr 3652 |
. . . 4
|
139 | | ssv 3625 |
. . . . . . . . . 10
|
140 | | fnssres 6004 |
. . . . . . . . . 10
|
141 | 2, 139, 140 | mp2an 708 |
. . . . . . . . 9
|
142 | | fvres 6207 |
. . . . . . . . . . 11
|
143 | | xmstps 22258 |
. . . . . . . . . . . 12
|
144 | | eqid 2622 |
. . . . . . . . . . . . 13
|
145 | 144 | tpstop 20741 |
. . . . . . . . . . . 12
|
146 | 143, 145 | syl 17 |
. . . . . . . . . . 11
|
147 | 142, 146 | eqeltrd 2701 |
. . . . . . . . . 10
|
148 | 147 | rgen 2922 |
. . . . . . . . 9
|
149 | | ffnfv 6388 |
. . . . . . . . 9
|
150 | 141, 148,
149 | mpbir2an 955 |
. . . . . . . 8
|
151 | | fco2 6059 |
. . . . . . . 8
|
152 | 150, 3, 151 | sylancr 695 |
. . . . . . 7
|
153 | | eqid 2622 |
. . . . . . . 8
|
154 | 10, 153 | ptbasfi 21384 |
. . . . . . 7
|
155 | 1, 152, 154 | syl2anc 693 |
. . . . . 6
|
156 | | eqid 2622 |
. . . . . . . . 9
|
157 | 156 | mopntop 22245 |
. . . . . . . 8
|
158 | 18, 157 | syl 17 |
. . . . . . 7
|
159 | 14, 17, 15, 1, 5 | prdsbas2 16129 |
. . . . . . . . . . . 12
|
160 | 3, 74 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
161 | 3 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
162 | | xmstps 22258 |
. . . . . . . . . . . . . . . . . 18
|
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
164 | 36, 73 | istps 20738 |
. . . . . . . . . . . . . . . . 17
TopOn |
165 | 163, 164 | sylib 208 |
. . . . . . . . . . . . . . . 16
TopOn |
166 | 160, 165 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
TopOn |
167 | | toponuni 20719 |
. . . . . . . . . . . . . . 15
TopOn |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . . 14
|
169 | 36, 168 | syl5eqr 2670 |
. . . . . . . . . . . . 13
|
170 | 169 | ixpeq2dva 7923 |
. . . . . . . . . . . 12
|
171 | 159, 170 | eqtrd 2656 |
. . . . . . . . . . 11
|
172 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
173 | 172 | unieqd 4446 |
. . . . . . . . . . . 12
|
174 | 173 | cbvixpv 7926 |
. . . . . . . . . . 11
|
175 | 171, 174 | syl6eq 2672 |
. . . . . . . . . 10
|
176 | 156 | mopntopon 22244 |
. . . . . . . . . . . 12
TopOn |
177 | 18, 176 | syl 17 |
. . . . . . . . . . 11
TopOn |
178 | | toponmax 20730 |
. . . . . . . . . . 11
TopOn |
179 | 177, 178 | syl 17 |
. . . . . . . . . 10
|
180 | 175, 179 | eqeltrrd 2702 |
. . . . . . . . 9
|
181 | 180 | snssd 4340 |
. . . . . . . 8
|
182 | 175 | mpteq1d 4738 |
. . . . . . . . . . . . . . . . . 18
|
183 | 182 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
184 | 183 | cnveqd 5298 |
. . . . . . . . . . . . . . . 16
|
185 | 184 | imaeq1d 5465 |
. . . . . . . . . . . . . . 15
|
186 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . 20
|
187 | 186 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
188 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
189 | 188 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . 19
|
190 | 187, 189 | elrab2 3366 |
. . . . . . . . . . . . . . . . . 18
|
191 | 161, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
192 | 191 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
193 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
|
194 | 161, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
195 | 194 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
196 | 193, 195 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . 21
|
197 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . 21
|
198 | 55 | mopni2 22298 |
. . . . . . . . . . . . . . . . . . . . 21
|
199 | 192, 196,
197, 198 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
200 | 18 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
|
201 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
202 | 201 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
203 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
204 | 203 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
|
205 | 156 | blopn 22305 |
. . . . . . . . . . . . . . . . . . . . . 22
|
206 | 200, 202,
204, 205 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
|
207 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
|
208 | | blcntr 22218 |
. . . . . . . . . . . . . . . . . . . . . 22
|
209 | 200, 202,
207, 208 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
|
210 | | blssm 22223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
211 | 200, 202,
204, 210 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
212 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
213 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
214 | | rpgt0 11844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
215 | 214 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
216 | 213, 202,
204, 215, 97 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
217 | 216 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
218 | 217 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
219 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
220 | 219 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
221 | 220 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
222 | 218, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
223 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
224 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
225 | 222, 223,
224 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
226 | 212, 225 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
227 | 211, 226 | ssrabdv 3681 |
. . . . . . . . . . . . . . . . . . . . . 22
|
228 | 227, 189 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . . . . . 21
|
229 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
230 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
231 | 229, 230 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
|
232 | 231 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . 21
|
233 | 206, 209,
228, 232 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . 20
|
234 | 199, 233 | rexlimddv 3035 |
. . . . . . . . . . . . . . . . . . 19
|
235 | 234 | expr 643 |
. . . . . . . . . . . . . . . . . 18
|
236 | 190, 235 | syl5bi 232 |
. . . . . . . . . . . . . . . . 17
|
237 | 236 | ralrimiv 2965 |
. . . . . . . . . . . . . . . 16
|
238 | 158 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
239 | | eltop2 20779 |
. . . . . . . . . . . . . . . . 17
|
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . 16
|
241 | 237, 240 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
242 | 185, 241 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
|
243 | 242 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
244 | 160 | raleqdv 3144 |
. . . . . . . . . . . . 13
|
245 | 243, 244 | mpbird 247 |
. . . . . . . . . . . 12
|
246 | 245 | ralrimiva 2966 |
. . . . . . . . . . 11
|
247 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
248 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
249 | 248 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
250 | 249 | cnveqd 5298 |
. . . . . . . . . . . . . . 15
|
251 | 250 | imaeq1d 5465 |
. . . . . . . . . . . . . 14
|
252 | 251 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
253 | 247, 252 | raleqbidv 3152 |
. . . . . . . . . . . 12
|
254 | 253 | cbvralv 3171 |
. . . . . . . . . . 11
|
255 | 246, 254 | sylib 208 |
. . . . . . . . . 10
|
256 | | eqid 2622 |
. . . . . . . . . . 11
|
257 | 256 | fmpt2x 7236 |
. . . . . . . . . 10
|
258 | 255, 257 | sylib 208 |
. . . . . . . . 9
|
259 | | frn 6053 |
. . . . . . . . 9
|
260 | 258, 259 | syl 17 |
. . . . . . . 8
|
261 | 181, 260 | unssd 3789 |
. . . . . . 7
|
262 | | fiss 8330 |
. . . . . . 7
|
263 | 158, 261,
262 | syl2anc 693 |
. . . . . 6
|
264 | 155, 263 | eqsstrd 3639 |
. . . . 5
|
265 | | fitop 20705 |
. . . . . . 7
|
266 | 158, 265 | syl 17 |
. . . . . 6
|
267 | 156 | mopnval 22243 |
. . . . . . . 8
|
268 | 18, 267 | syl 17 |
. . . . . . 7
|
269 | | tgdif0 20796 |
. . . . . . 7
|
270 | 268, 269 | syl6eqr 2674 |
. . . . . 6
|
271 | 266, 270 | eqtrd 2656 |
. . . . 5
|
272 | 264, 271 | sseqtrd 3641 |
. . . 4
|
273 | | 2basgen 20794 |
. . . 4
|
274 | 138, 272,
273 | syl2anc 693 |
. . 3
|
275 | 12, 274 | eqtr4d 2659 |
. 2
|
276 | | prdsxms.j |
. . 3
|
277 | 14, 15, 1, 5, 276 | prdstopn 21431 |
. 2
|
278 | 275, 277,
270 | 3eqtr4d 2666 |
1
|