Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . 4
|
2 | 1 | rnex 7100 |
. . 3
|
3 | | ssid 3624 |
. . . . 5
|
4 | | dfac12.1 |
. . . . . 6
|
5 | | sseq1 3626 |
. . . . . . . . 9
|
6 | | fveq2 6191 |
. . . . . . . . . . 11
|
7 | | f1eq1 6096 |
. . . . . . . . . . 11
|
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
|
9 | | fveq2 6191 |
. . . . . . . . . . 11
|
10 | | f1eq2 6097 |
. . . . . . . . . . 11
|
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
|
12 | 8, 11 | bitrd 268 |
. . . . . . . . 9
|
13 | 5, 12 | imbi12d 334 |
. . . . . . . 8
|
14 | 13 | imbi2d 330 |
. . . . . . 7
|
15 | | sseq1 3626 |
. . . . . . . . 9
|
16 | | fveq2 6191 |
. . . . . . . . . . 11
|
17 | | f1eq1 6096 |
. . . . . . . . . . 11
|
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
|
19 | | fveq2 6191 |
. . . . . . . . . . 11
|
20 | | f1eq2 6097 |
. . . . . . . . . . 11
|
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
|
22 | 18, 21 | bitrd 268 |
. . . . . . . . 9
|
23 | 15, 22 | imbi12d 334 |
. . . . . . . 8
|
24 | 23 | imbi2d 330 |
. . . . . . 7
|
25 | | r19.21v 2960 |
. . . . . . . 8
|
26 | | eloni 5733 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
|
28 | | ordelss 5739 |
. . . . . . . . . . . . . . . . 17
|
29 | 27, 28 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
30 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | sstrd 3613 |
. . . . . . . . . . . . . . 15
|
32 | | pm5.5 351 |
. . . . . . . . . . . . . . 15
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
|
34 | 33 | ralbidva 2985 |
. . . . . . . . . . . . 13
|
35 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
36 | | dfac12.3 |
. . . . . . . . . . . . . . . 16
har |
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
har |
38 | | dfac12.4 |
. . . . . . . . . . . . . . 15
recs OrdIso |
39 | | simplrl 800 |
. . . . . . . . . . . . . . 15
|
40 | | eqid 2622 |
. . . . . . . . . . . . . . 15
OrdIso OrdIso |
41 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
42 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
43 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
44 | | f1eq1 6096 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
47 | | f1eq2 6097 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
49 | 45, 48 | bitrd 268 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
|
51 | 42, 50 | sylib 208 |
. . . . . . . . . . . . . . 15
|
52 | 35, 37, 38, 39, 40, 41, 51 | dfac12lem2 8966 |
. . . . . . . . . . . . . 14
|
53 | 52 | ex 450 |
. . . . . . . . . . . . 13
|
54 | 34, 53 | sylbid 230 |
. . . . . . . . . . . 12
|
55 | 54 | expr 643 |
. . . . . . . . . . 11
|
56 | 55 | com23 86 |
. . . . . . . . . 10
|
57 | 56 | expcom 451 |
. . . . . . . . 9
|
58 | 57 | a2d 29 |
. . . . . . . 8
|
59 | 25, 58 | syl5bi 232 |
. . . . . . 7
|
60 | 14, 24, 59 | tfis3 7057 |
. . . . . 6
|
61 | 4, 60 | mpcom 38 |
. . . . 5
|
62 | 3, 61 | mpi 20 |
. . . 4
|
63 | | f1f 6101 |
. . . 4
|
64 | | frn 6053 |
. . . 4
|
65 | 62, 63, 64 | 3syl 18 |
. . 3
|
66 | | onssnum 8863 |
. . 3
|
67 | 2, 65, 66 | sylancr 695 |
. 2
|
68 | | f1f1orn 6148 |
. . . 4
|
69 | 62, 68 | syl 17 |
. . 3
|
70 | | fvex 6201 |
. . . 4
|
71 | 70 | f1oen 7976 |
. . 3
|
72 | | ennum 8773 |
. . 3
|
73 | 69, 71, 72 | 3syl 18 |
. 2
|
74 | 67, 73 | mpbird 247 |
1
|