Step | Hyp | Ref
| Expression |
1 | | inawina 9089 |
. . . . . 6
|
2 | | winaon 9087 |
. . . . . 6
|
3 | 1, 2 | syl 16 |
. . . . 5
|
4 | | winalim 9094 |
. . . . . 6
|
5 | 1, 4 | syl 16 |
. . . . 5
|
6 | | r1lim 8211 |
. . . . 5
|
7 | 3, 5, 6 | syl2anc 661 |
. . . 4
|
8 | | onelon 4908 |
. . . . . . . . 9
|
9 | 3, 8 | sylan 471 |
. . . . . . . 8
|
10 | | eleq1 2529 |
. . . . . . . . . . 11
|
11 | | fveq2 5871 |
. . . . . . . . . . . 12
|
12 | 11 | breq1d 4462 |
. . . . . . . . . . 11
|
13 | 10, 12 | imbi12d 320 |
. . . . . . . . . 10
|
14 | | eleq1 2529 |
. . . . . . . . . . 11
|
15 | | fveq2 5871 |
. . . . . . . . . . . 12
|
16 | 15 | breq1d 4462 |
. . . . . . . . . . 11
|
17 | 14, 16 | imbi12d 320 |
. . . . . . . . . 10
|
18 | | eleq1 2529 |
. . . . . . . . . . 11
|
19 | | fveq2 5871 |
. . . . . . . . . . . 12
|
20 | 19 | breq1d 4462 |
. . . . . . . . . . 11
|
21 | 18, 20 | imbi12d 320 |
. . . . . . . . . 10
|
22 | | ne0i 3790 |
. . . . . . . . . . . . 13
|
23 | | 0sdomg 7666 |
. . . . . . . . . . . . 13
|
24 | 22, 23 | syl5ibr 221 |
. . . . . . . . . . . 12
|
25 | | r10 8207 |
. . . . . . . . . . . . 13
|
26 | 25 | breq1i 4459 |
. . . . . . . . . . . 12
|
27 | 24, 26 | syl6ibr 227 |
. . . . . . . . . . 11
|
28 | 1, 2, 27 | 3syl 20 |
. . . . . . . . . 10
|
29 | | eloni 4893 |
. . . . . . . . . . . . . . 15
|
30 | | ordtr 4897 |
. . . . . . . . . . . . . . 15
|
31 | 29, 30 | syl 16 |
. . . . . . . . . . . . . 14
|
32 | | trsuc 4967 |
. . . . . . . . . . . . . . 15
|
33 | 32 | ex 434 |
. . . . . . . . . . . . . 14
|
34 | 3, 31, 33 | 3syl 20 |
. . . . . . . . . . . . 13
|
35 | 34 | adantl 466 |
. . . . . . . . . . . 12
|
36 | | r1suc 8209 |
. . . . . . . . . . . . . . 15
|
37 | | fvex 5881 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | cardid 8943 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | ensymi 7585 |
. . . . . . . . . . . . . . . 16
|
40 | | pwen 7710 |
. . . . . . . . . . . . . . . 16
|
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
42 | 36, 41 | syl6eqbr 4489 |
. . . . . . . . . . . . . 14
|
43 | | winacard 9091 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | eleq2d 2527 |
. . . . . . . . . . . . . . . . . 18
|
45 | | cardsdom 8951 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 37, 2, 45 | sylancr 663 |
. . . . . . . . . . . . . . . . . 18
|
47 | 44, 46 | bitr3d 255 |
. . . . . . . . . . . . . . . . 17
|
48 | 1, 47 | syl 16 |
. . . . . . . . . . . . . . . 16
|
49 | | elina 9086 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49 | simp3bi 1013 |
. . . . . . . . . . . . . . . . 17
|
51 | | pweq 4015 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51 | breq1d 4462 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | rspccv 3207 |
. . . . . . . . . . . . . . . . 17
|
54 | 50, 53 | syl 16 |
. . . . . . . . . . . . . . . 16
|
55 | 48, 54 | sylbird 235 |
. . . . . . . . . . . . . . 15
|
56 | 55 | imp 429 |
. . . . . . . . . . . . . 14
|
57 | | ensdomtr 7673 |
. . . . . . . . . . . . . 14
|
58 | 42, 56, 57 | syl2an 477 |
. . . . . . . . . . . . 13
|
59 | 58 | expr 615 |
. . . . . . . . . . . 12
|
60 | 35, 59 | imim12d 74 |
. . . . . . . . . . 11
|
61 | 60 | ex 434 |
. . . . . . . . . 10
|
62 | | vex 3112 |
. . . . . . . . . . . . . . . 16
|
63 | | r1lim 8211 |
. . . . . . . . . . . . . . . 16
|
64 | 62, 63 | mpan 670 |
. . . . . . . . . . . . . . 15
|
65 | | nfcv 2619 |
. . . . . . . . . . . . . . . . . . 19
|
66 | | nfcv 2619 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | | nfcv 2619 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | | nfiu1 4360 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 66, 67, 68 | nfbr 4496 |
. . . . . . . . . . . . . . . . . . 19
|
70 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 70 | breq1d 4462 |
. . . . . . . . . . . . . . . . . . 19
|
72 | | fvex 5881 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | 62, 72 | iunex 6780 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | ssiun2 4373 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | | ssdomg 7581 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | 73, 74, 75 | mpsyl 63 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | | endomtr 7593 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 39, 76, 77 | sylancr 663 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 65, 69, 71, 78 | vtoclgaf 3172 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | rgen 2817 |
. . . . . . . . . . . . . . . . 17
|
81 | | iundom 8938 |
. . . . . . . . . . . . . . . . 17
|
82 | 62, 80, 81 | mp2an 672 |
. . . . . . . . . . . . . . . 16
|
83 | 62, 73 | unex 6598 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | | ssun2 3667 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | ssdomg 7581 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 83, 84, 85 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 62 | xpdom2 7632 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
89 | | ssun1 3666 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | | ssdomg 7581 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | 83, 89, 90 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
|
92 | 83 | xpdom1 7636 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
94 | | domtr 7588 |
. . . . . . . . . . . . . . . . . 18
|
95 | 88, 93, 94 | mp2an 672 |
. . . . . . . . . . . . . . . . 17
|
96 | | limomss 6705 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 96, 89 | syl6ss 3515 |
. . . . . . . . . . . . . . . . . . 19
|
98 | | ssdomg 7581 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 83, 97, 98 | mpsyl 63 |
. . . . . . . . . . . . . . . . . 18
|
100 | | infxpidm 8958 |
. . . . . . . . . . . . . . . . . 18
|
101 | 99, 100 | syl 16 |
. . . . . . . . . . . . . . . . 17
|
102 | | domentr 7594 |
. . . . . . . . . . . . . . . . 17
|
103 | 95, 101, 102 | sylancr 663 |
. . . . . . . . . . . . . . . 16
|
104 | | domtr 7588 |
. . . . . . . . . . . . . . . 16
|
105 | 82, 103, 104 | sylancr 663 |
. . . . . . . . . . . . . . 15
|
106 | 64, 105 | eqbrtrd 4472 |
. . . . . . . . . . . . . 14
|
107 | 106 | ad2antlr 726 |
. . . . . . . . . . . . 13
|
108 | | eleq1a 2540 |
. . . . . . . . . . . . . . . . . . 19
|
109 | | ordirr 4901 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 3, 29, 109 | 3syl 20 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 108, 110 | nsyli 141 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | imp 429 |
. . . . . . . . . . . . . . . . 17
|
113 | 112 | ad2ant2r 746 |
. . . . . . . . . . . . . . . 16
|
114 | | simpll 753 |
. . . . . . . . . . . . . . . . 17
|
115 | | limord 4942 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
116 | 62 | elon 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
117 | 115, 116 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 117 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | | cardf 8946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
120 | | r1fnon 8206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
121 | | dffn2 5737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
122 | 120, 121 | mpbi 208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
123 | | fco 5746 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
124 | 119, 122,
123 | mp2an 672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
125 | | onss 6626 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
126 | | fssres 5756 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
127 | 124, 125,
126 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
128 | | ffn 5736 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
129 | 118, 127,
128 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . 22
|
130 | 3 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
131 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
132 | | simplll 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
133 | | ontr1 4929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
134 | 133 | imp 429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
135 | 130, 131,
132, 134 | syl12anc 1226 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
136 | 37, 130, 45 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
137 | 1, 43 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
138 | 137 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
139 | 138 | eleq2d 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
140 | 136, 139 | bitr3d 255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
141 | 140 | biimpd 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
142 | 135, 141 | embantd 54 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
143 | 117 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
144 | | fvres 5885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
145 | 144 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
146 | | onelon 4908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
147 | | fvco3 5950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
148 | 122, 146,
147 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
149 | 145, 148 | eqtrd 2498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
150 | 143, 149 | sylan 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | 150 | eleq1d 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
152 | 142, 151 | sylibrd 234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
153 | 152 | ralimdva 2865 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
154 | 153 | impr 619 |
. . . . . . . . . . . . . . . . . . . . . 22
|
155 | | ffnfv 6057 |
. . . . . . . . . . . . . . . . . . . . . 22
|
156 | 129, 154,
155 | sylanbrc 664 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | | eleq2 2530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
158 | 157 | biimpa 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
159 | | eliun 4335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
160 | | cardon 8346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
161 | 160 | onelssi 4991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
162 | 149 | sseq2d 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
163 | 161, 162 | syl5ibr 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
164 | 163 | reximdva 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
165 | 159, 164 | syl5bi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
166 | 158, 165 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
167 | 166 | expdimp 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
168 | 167 | ralrimiv 2869 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
169 | 168 | ex 434 |
. . . . . . . . . . . . . . . . . . . . . 22
|
170 | 118, 169 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
|
171 | | ffun 5738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
172 | 124, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
173 | | resfunexg 6137 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
174 | 172, 62, 173 | mp2an 672 |
. . . . . . . . . . . . . . . . . . . . . 22
|
175 | | feq1 5718 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
176 | | fveq1 5870 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
177 | 176 | sseq2d 3531 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
178 | 177 | rexbidv 2968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
179 | 178 | ralbidv 2896 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
180 | 175, 179 | anbi12d 710 |
. . . . . . . . . . . . . . . . . . . . . 22
|
181 | 174, 180 | spcev 3201 |
. . . . . . . . . . . . . . . . . . . . 21
|
182 | 156, 170,
181 | syl6an 545 |
. . . . . . . . . . . . . . . . . . . 20
|
183 | 3 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
|
184 | | cfflb 8660 |
. . . . . . . . . . . . . . . . . . . . 21
|
185 | 183, 118,
184 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
|
186 | 182, 185 | syld 44 |
. . . . . . . . . . . . . . . . . . 19
|
187 | 49 | simp2bi 1012 |
. . . . . . . . . . . . . . . . . . . . 21
|
188 | 187 | sseq1d 3530 |
. . . . . . . . . . . . . . . . . . . 20
|
189 | 188 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
|
190 | 186, 189 | sylibd 214 |
. . . . . . . . . . . . . . . . . 18
|
191 | | ontri1 4917 |
. . . . . . . . . . . . . . . . . . 19
|
192 | 183, 118,
191 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
|
193 | 190, 192 | sylibd 214 |
. . . . . . . . . . . . . . . . 17
|
194 | 114, 193 | mt2d 117 |
. . . . . . . . . . . . . . . 16
|
195 | 62, 72 | iunonOLD 7029 |
. . . . . . . . . . . . . . . . . 18
|
196 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
197 | 195, 196 | mprg 2820 |
. . . . . . . . . . . . . . . . 17
|
198 | | eqcom 2466 |
. . . . . . . . . . . . . . . . . 18
|
199 | | eloni 4893 |
. . . . . . . . . . . . . . . . . . 19
|
200 | | eloni 4893 |
. . . . . . . . . . . . . . . . . . 19
|
201 | | ordequn 4983 |
. . . . . . . . . . . . . . . . . . 19
|
202 | 199, 200,
201 | syl2an 477 |
. . . . . . . . . . . . . . . . . 18
|
203 | 198, 202 | syl5bi 217 |
. . . . . . . . . . . . . . . . 17
|
204 | 118, 197,
203 | sylancl 662 |
. . . . . . . . . . . . . . . 16
|
205 | 113, 194,
204 | mtord 660 |
. . . . . . . . . . . . . . 15
|
206 | | onelss 4925 |
. . . . . . . . . . . . . . . . . . . 20
|
207 | 183, 114,
206 | sylc 60 |
. . . . . . . . . . . . . . . . . . 19
|
208 | | onelss 4925 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
209 | 130, 142,
208 | sylsyld 56 |
. . . . . . . . . . . . . . . . . . . . . 22
|
210 | 209 | ralimdva 2865 |
. . . . . . . . . . . . . . . . . . . . 21
|
211 | 210 | impr 619 |
. . . . . . . . . . . . . . . . . . . 20
|
212 | | iunss 4371 |
. . . . . . . . . . . . . . . . . . . 20
|
213 | 211, 212 | sylibr 212 |
. . . . . . . . . . . . . . . . . . 19
|
214 | 207, 213 | unssd 3679 |
. . . . . . . . . . . . . . . . . 18
|
215 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
216 | | iuneq1 4344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
217 | 215, 216 | uneq12d 3658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
218 | 217 | eleq1d 2526 |
. . . . . . . . . . . . . . . . . . . . . 22
|
219 | | 0elon 4936 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
220 | 219 | elimel 4004 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
221 | 220 | elexi 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
222 | 221, 72 | iunonOLD 7029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
223 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
224 | 222, 223 | mprg 2820 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
225 | 220, 224 | onun2i 4998 |
. . . . . . . . . . . . . . . . . . . . . 22
|
226 | 218, 225 | dedth 3993 |
. . . . . . . . . . . . . . . . . . . . 21
|
227 | 117, 226 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
|
228 | 227 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
|
229 | 3 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
|
230 | | onsseleq 4924 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 228, 229,
230 | syl2an 477 |
. . . . . . . . . . . . . . . . . 18
|
232 | 214, 231 | mpbid 210 |
. . . . . . . . . . . . . . . . 17
|
233 | 232 | orcomd 388 |
. . . . . . . . . . . . . . . 16
|
234 | 233 | ord 377 |
. . . . . . . . . . . . . . 15
|
235 | 205, 234 | mpd 15 |
. . . . . . . . . . . . . 14
|
236 | 137 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
|
237 | | iscard 8377 |
. . . . . . . . . . . . . . . 16
|
238 | 237 | simprbi 464 |
. . . . . . . . . . . . . . 15
|
239 | | breq1 4455 |
. . . . . . . . . . . . . . . 16
|
240 | 239 | rspccv 3207 |
. . . . . . . . . . . . . . 15
|
241 | 236, 238,
240 | 3syl 20 |
. . . . . . . . . . . . . 14
|
242 | 235, 241 | mpd 15 |
. . . . . . . . . . . . 13
|
243 | | domsdomtr 7672 |
. . . . . . . . . . . . 13
|
244 | 107, 242,
243 | syl2anc 661 |
. . . . . . . . . . . 12
|
245 | 244 | exp43 612 |
. . . . . . . . . . 11
|
246 | 245 | com4l 84 |
. . . . . . . . . 10
|
247 | 13, 17, 21, 28, 61, 246 | tfinds2 6698 |
. . . . . . . . 9
|
248 | 247 | impd 431 |
. . . . . . . 8
|
249 | 9, 248 | mpcom 36 |
. . . . . . 7
|
250 | | sdomdom 7563 |
. . . . . . 7
|
251 | 249, 250 | syl 16 |
. . . . . 6
|
252 | 251 | ralrimiva 2871 |
. . . . 5
|
253 | | iundom 8938 |
. . . . 5
|
254 | 3, 252, 253 | syl2anc 661 |
. . . 4
|
255 | 7, 254 | eqbrtrd 4472 |
. . 3
|
256 | | winainf 9093 |
. . . . 5
|
257 | 1, 256 | syl 16 |
. . . 4
|
258 | | infxpen 8413 |
. . . 4
|
259 | 3, 257, 258 | syl2anc 661 |
. . 3
|
260 | | domentr 7594 |
. . 3
|
261 | 255, 259,
260 | syl2anc 661 |
. 2
|
262 | | fvex 5881 |
. . 3
|
263 | 122 | fdmi 5741 |
. . . . 5
|
264 | 2, 263 | syl6eleqr 2556 |
. . . 4
|
265 | | onssr1 8270 |
. . . 4
|
266 | 1, 264, 265 | 3syl 20 |
. . 3
|
267 | | ssdomg 7581 |
. . 3
|
268 | 262, 266,
267 | mpsyl 63 |
. 2
|
269 | | sbth 7657 |
. 2
|
270 | 261, 268,
269 | syl2anc 661 |
1
|