Step | Hyp | Ref
| Expression |
1 | | rankwflemb 8656 |
. . . 4
|
2 | | harcl 8466 |
. . . . . . . . 9
har |
3 | | pweq 4161 |
. . . . . . . . . . 11
har har |
4 | 3 | eleq1d 2686 |
. . . . . . . . . 10
har
har |
5 | 4 | rspcv 3305 |
. . . . . . . . 9
har
har |
6 | 2, 5 | ax-mp 5 |
. . . . . . . 8
har |
7 | | cardid2 8779 |
. . . . . . . 8
har
har har |
8 | | ensym 8005 |
. . . . . . . 8
har har har har |
9 | | bren 7964 |
. . . . . . . . 9
har har
harhar |
10 | | simpr 477 |
. . . . . . . . . . . 12
harhar |
11 | | f1of1 6136 |
. . . . . . . . . . . . . 14
harhar harhar |
12 | 11 | adantr 481 |
. . . . . . . . . . . . 13
harhar harhar |
13 | | cardon 8770 |
. . . . . . . . . . . . . 14
har |
14 | 13 | onssi 7037 |
. . . . . . . . . . . . 13
har
|
15 | | f1ss 6106 |
. . . . . . . . . . . . 13
harhar har
har |
16 | 12, 14, 15 | sylancl 694 |
. . . . . . . . . . . 12
harhar har |
17 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
18 | 17 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
19 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . 21
|
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
21 | 20 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 21, 22 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . 18
|
24 | 18, 23 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
25 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . 18
OrdIso OrdIso |
26 | 25 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
OrdIso OrdIso |
27 | 24, 26 | ifeq12d 4106 |
. . . . . . . . . . . . . . . 16
OrdIso
OrdIso |
28 | 27 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
OrdIso OrdIso |
29 | | dmeq 5324 |
. . . . . . . . . . . . . . . . 17
|
30 | 29 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
31 | 29 | unieqd 4446 |
. . . . . . . . . . . . . . . . . 18
|
32 | 29, 31 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
33 | | rneq 5351 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
34 | 33 | unieqd 4446 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 34 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | unieqd 4446 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 38 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
40 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 40 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . 18
|
42 | 39, 41 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
43 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | 43, 31 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 44 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | | oieq2 8418 |
. . . . . . . . . . . . . . . . . . . . . 22
OrdIso OrdIso |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
OrdIso OrdIso |
48 | 47 | cnveqd 5298 |
. . . . . . . . . . . . . . . . . . . 20
OrdIso OrdIso |
49 | 48, 44 | coeq12d 5286 |
. . . . . . . . . . . . . . . . . . 19
OrdIso OrdIso |
50 | 49 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . 18
OrdIso OrdIso |
51 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
OrdIso OrdIso |
52 | 32, 42, 51 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . 16
OrdIso
OrdIso |
53 | 30, 52 | mpteq12dv 4733 |
. . . . . . . . . . . . . . 15
OrdIso
OrdIso |
54 | 28, 53 | syl5eq 2668 |
. . . . . . . . . . . . . 14
OrdIso
OrdIso |
55 | 54 | cbvmptv 4750 |
. . . . . . . . . . . . 13
OrdIso
OrdIso |
56 | | recseq 7470 |
. . . . . . . . . . . . 13
OrdIso
OrdIso recs
OrdIso recs
OrdIso |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . 12
recs
OrdIso recs
OrdIso |
58 | 10, 16, 57 | dfac12lem3 8967 |
. . . . . . . . . . 11
harhar |
59 | 58 | ex 450 |
. . . . . . . . . 10
harhar
|
60 | 59 | exlimiv 1858 |
. . . . . . . . 9
harhar
|
61 | 9, 60 | sylbi 207 |
. . . . . . . 8
har har |
62 | 6, 7, 8, 61 | 4syl 19 |
. . . . . . 7
|
63 | 62 | imp 445 |
. . . . . 6
|
64 | | r1suc 8633 |
. . . . . . . . 9
|
65 | 64 | adantl 482 |
. . . . . . . 8
|
66 | 65 | eleq2d 2687 |
. . . . . . 7
|
67 | | elpwi 4168 |
. . . . . . 7
|
68 | 66, 67 | syl6bi 243 |
. . . . . 6
|
69 | | ssnum 8862 |
. . . . . 6
|
70 | 63, 68, 69 | syl6an 568 |
. . . . 5
|
71 | 70 | rexlimdva 3031 |
. . . 4
|
72 | 1, 71 | syl5bi 232 |
. . 3
|
73 | 72 | ssrdv 3609 |
. 2
|
74 | | onwf 8693 |
. . . . . 6
|
75 | 74 | sseli 3599 |
. . . . 5
|
76 | | pwwf 8670 |
. . . . 5
|
77 | 75, 76 | sylib 208 |
. . . 4
|
78 | | ssel 3597 |
. . . 4
|
79 | 77, 78 | syl5 34 |
. . 3
|
80 | 79 | ralrimiv 2965 |
. 2
|
81 | 73, 80 | impbii 199 |
1
|