Proof of Theorem dfac12lem2
Step | Hyp | Ref
| Expression |
1 | | dfac12.4 |
. . . . . . . . . . . . . 14
recs OrdIso |
2 | 1 | tfr1 7493 |
. . . . . . . . . . . . 13
|
3 | | fnfun 5988 |
. . . . . . . . . . . . 13
|
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . 12
|
5 | | dfac12.5 |
. . . . . . . . . . . 12
|
6 | | funimaexg 5975 |
. . . . . . . . . . . 12
|
7 | 4, 5, 6 | sylancr 695 |
. . . . . . . . . . 11
|
8 | | uniexg 6955 |
. . . . . . . . . . 11
|
9 | | rnexg 7098 |
. . . . . . . . . . 11
|
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . 10
|
11 | | dfac12.8 |
. . . . . . . . . . . . . . 15
|
12 | | f1f 6101 |
. . . . . . . . . . . . . . . . 17
|
13 | | fssxp 6060 |
. . . . . . . . . . . . . . . . 17
|
14 | | ssv 3625 |
. . . . . . . . . . . . . . . . . . . 20
|
15 | | xpss1 5228 |
. . . . . . . . . . . . . . . . . . . 20
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
17 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . 19
|
18 | 16, 17 | mpan2 707 |
. . . . . . . . . . . . . . . . . 18
|
19 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | elpw 4164 |
. . . . . . . . . . . . . . . . . 18
|
21 | 18, 20 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
22 | 12, 13, 21 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
23 | 22 | ralimi 2952 |
. . . . . . . . . . . . . . 15
|
24 | 11, 23 | syl 17 |
. . . . . . . . . . . . . 14
|
25 | | onss 6990 |
. . . . . . . . . . . . . . . . 17
|
26 | 5, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
|
27 | | fndm 5990 |
. . . . . . . . . . . . . . . . 17
|
28 | 2, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
29 | 26, 28 | syl6sseqr 3652 |
. . . . . . . . . . . . . . 15
|
30 | | funimass4 6247 |
. . . . . . . . . . . . . . 15
|
31 | 4, 29, 30 | sylancr 695 |
. . . . . . . . . . . . . 14
|
32 | 24, 31 | mpbird 247 |
. . . . . . . . . . . . 13
|
33 | | sspwuni 4611 |
. . . . . . . . . . . . 13
|
34 | 32, 33 | sylib 208 |
. . . . . . . . . . . 12
|
35 | | rnss 5354 |
. . . . . . . . . . . 12
|
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
|
37 | | rnxpss 5566 |
. . . . . . . . . . 11
|
38 | 36, 37 | syl6ss 3615 |
. . . . . . . . . 10
|
39 | | ssonuni 6986 |
. . . . . . . . . 10
|
40 | 10, 38, 39 | sylc 65 |
. . . . . . . . 9
|
41 | | suceloni 7013 |
. . . . . . . . 9
|
42 | 40, 41 | syl 17 |
. . . . . . . 8
|
43 | 42 | ad2antrr 762 |
. . . . . . 7
|
44 | | rankon 8658 |
. . . . . . 7
|
45 | | omcl 7616 |
. . . . . . 7
|
46 | 43, 44, 45 | sylancl 694 |
. . . . . 6
|
47 | | rankr1ai 8661 |
. . . . . . . . . . . 12
|
48 | 47 | ad2antlr 763 |
. . . . . . . . . . 11
|
49 | | simpr 477 |
. . . . . . . . . . 11
|
50 | 48, 49 | eleqtrd 2703 |
. . . . . . . . . 10
|
51 | | eloni 5733 |
. . . . . . . . . . . . 13
|
52 | 5, 51 | syl 17 |
. . . . . . . . . . . 12
|
53 | 52 | ad2antrr 762 |
. . . . . . . . . . 11
|
54 | | ordsucuniel 7024 |
. . . . . . . . . . 11
|
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
|
56 | 50, 55 | mpbid 222 |
. . . . . . . . 9
|
57 | 11 | ad2antrr 762 |
. . . . . . . . 9
|
58 | | fveq2 6191 |
. . . . . . . . . . . 12
|
59 | | f1eq1 6096 |
. . . . . . . . . . . 12
|
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
|
61 | | fveq2 6191 |
. . . . . . . . . . . 12
|
62 | | f1eq2 6097 |
. . . . . . . . . . . 12
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
|
64 | 60, 63 | bitrd 268 |
. . . . . . . . . 10
|
65 | 64 | rspcv 3305 |
. . . . . . . . 9
|
66 | 56, 57, 65 | sylc 65 |
. . . . . . . 8
|
67 | | f1f 6101 |
. . . . . . . 8
|
68 | 66, 67 | syl 17 |
. . . . . . 7
|
69 | | r1elwf 8659 |
. . . . . . . . 9
|
70 | 69 | ad2antlr 763 |
. . . . . . . 8
|
71 | | rankidb 8663 |
. . . . . . . 8
|
72 | 70, 71 | syl 17 |
. . . . . . 7
|
73 | 68, 72 | ffvelrnd 6360 |
. . . . . 6
|
74 | | oacl 7615 |
. . . . . 6
|
75 | 46, 73, 74 | syl2anc 693 |
. . . . 5
|
76 | | dfac12.3 |
. . . . . . . 8
har |
77 | | f1f 6101 |
. . . . . . . 8
har
har |
78 | 76, 77 | syl 17 |
. . . . . . 7
har |
79 | 78 | ad2antrr 762 |
. . . . . 6
har |
80 | | imassrn 5477 |
. . . . . . . 8
|
81 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
82 | 81 | rnex 7100 |
. . . . . . . . . . . . . 14
|
83 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
84 | | onuni 6993 |
. . . . . . . . . . . . . . . . . . 19
|
85 | | sucidg 5803 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 83, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
87 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | | orduniorsuc 7030 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 89 | orcanai 952 |
. . . . . . . . . . . . . . . . . 18
|
91 | 86, 90 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
|
92 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
93 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | | f1eq1 6096 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
96 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | | f1eq2 6097 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 95, 98 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
|
100 | 99 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
|
101 | 91, 92, 100 | sylc 65 |
. . . . . . . . . . . . . . . 16
|
102 | | f1f 6101 |
. . . . . . . . . . . . . . . 16
|
103 | | frn 6053 |
. . . . . . . . . . . . . . . 16
|
104 | 101, 102,
103 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
105 | | epweon 6983 |
. . . . . . . . . . . . . . 15
|
106 | | wess 5101 |
. . . . . . . . . . . . . . 15
|
107 | 104, 105,
106 | mpisyl 21 |
. . . . . . . . . . . . . 14
|
108 | | eqid 2622 |
. . . . . . . . . . . . . . 15
OrdIso OrdIso |
109 | 108 | oiiso 8442 |
. . . . . . . . . . . . . 14
OrdIso OrdIso
|
110 | 82, 107, 109 | sylancr 695 |
. . . . . . . . . . . . 13
OrdIso
OrdIso |
111 | | isof1o 6573 |
. . . . . . . . . . . . 13
OrdIso
OrdIso OrdIso
OrdIso |
112 | | f1ocnv 6149 |
. . . . . . . . . . . . 13
OrdIso OrdIso OrdIso OrdIso
|
113 | | f1of1 6136 |
. . . . . . . . . . . . 13
OrdIso OrdIso OrdIso OrdIso |
114 | 110, 111,
112, 113 | 4syl 19 |
. . . . . . . . . . . 12
OrdIso OrdIso |
115 | | f1f1orn 6148 |
. . . . . . . . . . . . 13
|
116 | | f1of1 6136 |
. . . . . . . . . . . . 13
|
117 | 101, 115,
116 | 3syl 18 |
. . . . . . . . . . . 12
|
118 | | f1co 6110 |
. . . . . . . . . . . 12
OrdIso OrdIso OrdIso OrdIso |
119 | 114, 117,
118 | syl2anc 693 |
. . . . . . . . . . 11
OrdIso OrdIso |
120 | | dfac12.h |
. . . . . . . . . . . 12
OrdIso |
121 | | f1eq1 6096 |
. . . . . . . . . . . 12
OrdIso
OrdIso OrdIso OrdIso |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . 11
OrdIso OrdIso OrdIso |
123 | 119, 122 | sylibr 224 |
. . . . . . . . . 10
OrdIso |
124 | | f1f 6101 |
. . . . . . . . . 10
OrdIso
OrdIso |
125 | | frn 6053 |
. . . . . . . . . 10
OrdIso
OrdIso |
126 | 123, 124,
125 | 3syl 18 |
. . . . . . . . 9
OrdIso |
127 | | harcl 8466 |
. . . . . . . . . . 11
har |
128 | 127 | onordi 5832 |
. . . . . . . . . 10
har |
129 | 108 | oion 8441 |
. . . . . . . . . . . 12
OrdIso |
130 | 82, 129 | mp1i 13 |
. . . . . . . . . . 11
OrdIso |
131 | 108 | oien 8443 |
. . . . . . . . . . . . 13
OrdIso |
132 | 82, 107, 131 | sylancr 695 |
. . . . . . . . . . . 12
OrdIso |
133 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
134 | 133 | f1oen 7976 |
. . . . . . . . . . . . . 14
|
135 | | ensym 8005 |
. . . . . . . . . . . . . 14
|
136 | 101, 115,
134, 135 | 4syl 19 |
. . . . . . . . . . . . 13
|
137 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
138 | | dfac12.1 |
. . . . . . . . . . . . . . . 16
|
139 | 138 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
140 | | dfac12.6 |
. . . . . . . . . . . . . . . . 17
|
141 | 140 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
142 | 141, 91 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
143 | | r1ord2 8644 |
. . . . . . . . . . . . . . 15
|
144 | 139, 142,
143 | sylc 65 |
. . . . . . . . . . . . . 14
|
145 | | ssdomg 8001 |
. . . . . . . . . . . . . 14
|
146 | 137, 144,
145 | mpsyl 68 |
. . . . . . . . . . . . 13
|
147 | | endomtr 8014 |
. . . . . . . . . . . . 13
|
148 | 136, 146,
147 | syl2anc 693 |
. . . . . . . . . . . 12
|
149 | | endomtr 8014 |
. . . . . . . . . . . 12
OrdIso OrdIso |
150 | 132, 148,
149 | syl2anc 693 |
. . . . . . . . . . 11
OrdIso |
151 | | elharval 8468 |
. . . . . . . . . . 11
OrdIso
har
OrdIso OrdIso |
152 | 130, 150,
151 | sylanbrc 698 |
. . . . . . . . . 10
OrdIso har |
153 | | ordelss 5739 |
. . . . . . . . . 10
har
OrdIso har
OrdIso har |
154 | 128, 152,
153 | sylancr 695 |
. . . . . . . . 9
OrdIso har |
155 | 126, 154 | sstrd 3613 |
. . . . . . . 8
har |
156 | 80, 155 | syl5ss 3614 |
. . . . . . 7
har |
157 | | fvex 6201 |
. . . . . . . 8
har |
158 | 157 | elpw2 4828 |
. . . . . . 7
har har |
159 | 156, 158 | sylibr 224 |
. . . . . 6
har |
160 | 79, 159 | ffvelrnd 6360 |
. . . . 5
|
161 | 75, 160 | ifclda 4120 |
. . . 4
|
162 | 161 | ex 450 |
. . 3
|
163 | | iftrue 4092 |
. . . . . . . 8
|
164 | | iftrue 4092 |
. . . . . . . 8
|
165 | 163, 164 | eqeq12d 2637 |
. . . . . . 7
|
166 | 165 | adantl 482 |
. . . . . 6
|
167 | 42 | ad2antrr 762 |
. . . . . . 7
|
168 | | nsuceq0 5805 |
. . . . . . . 8
|
169 | 168 | a1i 11 |
. . . . . . 7
|
170 | 44 | a1i 11 |
. . . . . . 7
|
171 | | onsucuni 7028 |
. . . . . . . . . . 11
|
172 | 38, 171 | syl 17 |
. . . . . . . . . 10
|
173 | 172 | ad2antrr 762 |
. . . . . . . . 9
|
174 | 2 | a1i 11 |
. . . . . . . . . . . 12
|
175 | 26 | ad2antrr 762 |
. . . . . . . . . . . 12
|
176 | | fnfvima 6496 |
. . . . . . . . . . . 12
|
177 | 174, 175,
56, 176 | syl3anc 1326 |
. . . . . . . . . . 11
|
178 | | elssuni 4467 |
. . . . . . . . . . 11
|
179 | | rnss 5354 |
. . . . . . . . . . 11
|
180 | 177, 178,
179 | 3syl 18 |
. . . . . . . . . 10
|
181 | | f1fn 6102 |
. . . . . . . . . . . 12
|
182 | 66, 181 | syl 17 |
. . . . . . . . . . 11
|
183 | | fnfvelrn 6356 |
. . . . . . . . . . 11
|
184 | 182, 72, 183 | syl2anc 693 |
. . . . . . . . . 10
|
185 | 180, 184 | sseldd 3604 |
. . . . . . . . 9
|
186 | 173, 185 | sseldd 3604 |
. . . . . . . 8
|
187 | 186 | adantlrr 757 |
. . . . . . 7
|
188 | | rankon 8658 |
. . . . . . . 8
|
189 | 188 | a1i 11 |
. . . . . . 7
|
190 | | eleq1 2689 |
. . . . . . . . . . . 12
|
191 | 190 | anbi2d 740 |
. . . . . . . . . . 11
|
192 | 191 | anbi1d 741 |
. . . . . . . . . 10
|
193 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
194 | | suceq 5790 |
. . . . . . . . . . . . . 14
|
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . 13
|
196 | 195 | fveq2d 6195 |
. . . . . . . . . . . 12
|
197 | | id 22 |
. . . . . . . . . . . 12
|
198 | 196, 197 | fveq12d 6197 |
. . . . . . . . . . 11
|
199 | 198 | eleq1d 2686 |
. . . . . . . . . 10
|
200 | 192, 199 | imbi12d 334 |
. . . . . . . . 9
|
201 | 200, 186 | chvarv 2263 |
. . . . . . . 8
|
202 | 201 | adantlrl 756 |
. . . . . . 7
|
203 | | omopth2 7664 |
. . . . . . 7
|
204 | 167, 169,
170, 187, 189, 202, 203 | syl222anc 1342 |
. . . . . 6
|
205 | 194 | adantl 482 |
. . . . . . . . . . . . 13
|
206 | 205 | fveq2d 6195 |
. . . . . . . . . . . 12
|
207 | 206 | fveq1d 6193 |
. . . . . . . . . . 11
|
208 | 207 | eqeq2d 2632 |
. . . . . . . . . 10
|
209 | 66 | adantlrr 757 |
. . . . . . . . . . . 12
|
210 | 209 | adantr 481 |
. . . . . . . . . . 11
|
211 | 72 | adantlrr 757 |
. . . . . . . . . . . 12
|
212 | 211 | adantr 481 |
. . . . . . . . . . 11
|
213 | | r1elwf 8659 |
. . . . . . . . . . . . . . 15
|
214 | | rankidb 8663 |
. . . . . . . . . . . . . . 15
|
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . 14
|
216 | 215 | ad2antll 765 |
. . . . . . . . . . . . 13
|
217 | 216 | ad2antrr 762 |
. . . . . . . . . . . 12
|
218 | 205 | fveq2d 6195 |
. . . . . . . . . . . 12
|
219 | 217, 218 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
220 | | f1fveq 6519 |
. . . . . . . . . . 11
|
221 | 210, 212,
219, 220 | syl12anc 1324 |
. . . . . . . . . 10
|
222 | 208, 221 | bitr3d 270 |
. . . . . . . . 9
|
223 | 222 | biimpd 219 |
. . . . . . . 8
|
224 | 223 | expimpd 629 |
. . . . . . 7
|
225 | 193, 198 | jca 554 |
. . . . . . 7
|
226 | 224, 225 | impbid1 215 |
. . . . . 6
|
227 | 166, 204,
226 | 3bitrd 294 |
. . . . 5
|
228 | | iffalse 4095 |
. . . . . . . 8
|
229 | | iffalse 4095 |
. . . . . . . 8
|
230 | 228, 229 | eqeq12d 2637 |
. . . . . . 7
|
231 | 230 | adantl 482 |
. . . . . 6
|
232 | 76 | ad2antrr 762 |
. . . . . . 7
har |
233 | 159 | adantlrr 757 |
. . . . . . 7
har |
234 | 191 | anbi1d 741 |
. . . . . . . . . 10
|
235 | | imaeq2 5462 |
. . . . . . . . . . 11
|
236 | 235 | eleq1d 2686 |
. . . . . . . . . 10
har
har |
237 | 234, 236 | imbi12d 334 |
. . . . . . . . 9
har
har |
238 | 237, 159 | chvarv 2263 |
. . . . . . . 8
har |
239 | 238 | adantlrl 756 |
. . . . . . 7
har |
240 | | f1fveq 6519 |
. . . . . . 7
har har har
|
241 | 232, 233,
239, 240 | syl12anc 1324 |
. . . . . 6
|
242 | 123 | adantlrr 757 |
. . . . . . 7
OrdIso |
243 | | simplrl 800 |
. . . . . . . . 9
|
244 | 90 | fveq2d 6195 |
. . . . . . . . . . 11
|
245 | | r1suc 8633 |
. . . . . . . . . . . 12
|
246 | 83, 84, 245 | 3syl 18 |
. . . . . . . . . . 11
|
247 | 244, 246 | eqtrd 2656 |
. . . . . . . . . 10
|
248 | 247 | adantlrr 757 |
. . . . . . . . 9
|
249 | 243, 248 | eleqtrd 2703 |
. . . . . . . 8
|
250 | 249 | elpwid 4170 |
. . . . . . 7
|
251 | | simplrr 801 |
. . . . . . . . 9
|
252 | 251, 248 | eleqtrd 2703 |
. . . . . . . 8
|
253 | 252 | elpwid 4170 |
. . . . . . 7
|
254 | | f1imaeq 6522 |
. . . . . . 7
OrdIso |
255 | 242, 250,
253, 254 | syl12anc 1324 |
. . . . . 6
|
256 | 231, 241,
255 | 3bitrd 294 |
. . . . 5
|
257 | 227, 256 | pm2.61dan 832 |
. . . 4
|
258 | 257 | ex 450 |
. . 3
|
259 | 162, 258 | dom2lem 7995 |
. 2
|
260 | 138, 76, 1, 5, 120 | dfac12lem1 8965 |
. . 3
|
261 | | f1eq1 6096 |
. . 3
|
262 | 260, 261 | syl 17 |
. 2
|
263 | 259, 262 | mpbird 247 |
1
|