Step | Hyp | Ref
| Expression |
1 | | fveq2 5871 |
. . . . . . . . . 10
|
2 | | id 22 |
. . . . . . . . . 10
|
3 | 1, 2 | eqeq12d 2479 |
. . . . . . . . 9
|
4 | 3 | rspcv 3206 |
. . . . . . . 8
|
5 | | cardon 8346 |
. . . . . . . . 9
|
6 | | eleq1 2529 |
. . . . . . . . 9
|
7 | 5, 6 | mpbii 211 |
. . . . . . . 8
|
8 | 4, 7 | syl6com 35 |
. . . . . . 7
|
9 | 8 | ssrdv 3509 |
. . . . . 6
|
10 | | ssonuni 6622 |
. . . . . 6
|
11 | 9, 10 | syl5 32 |
. . . . 5
|
12 | 11 | imp 429 |
. . . 4
|
13 | | cardonle 8359 |
. . . 4
|
14 | 12, 13 | syl 16 |
. . 3
|
15 | | cardon 8346 |
. . . . 5
|
16 | 15 | onirri 4989 |
. . . 4
|
17 | | eluni 4252 |
. . . . . . . 8
|
18 | | elssuni 4279 |
. . . . . . . . . . . . . . . . . 18
|
19 | | ssdomg 7581 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | adantl 466 |
. . . . . . . . . . . . . . . . . 18
|
21 | 18, 20 | syl5 32 |
. . . . . . . . . . . . . . . . 17
|
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
23 | | onenon 8351 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
25 | 22, 24 | syl6eqelr 2554 |
. . . . . . . . . . . . . . . . . 18
|
26 | | onenon 8351 |
. . . . . . . . . . . . . . . . . 18
|
27 | | carddom2 8379 |
. . . . . . . . . . . . . . . . . 18
|
28 | 25, 26, 27 | syl2an 477 |
. . . . . . . . . . . . . . . . 17
|
29 | 21, 28 | sylibrd 234 |
. . . . . . . . . . . . . . . 16
|
30 | | sseq1 3524 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
32 | 29, 31 | sylibd 214 |
. . . . . . . . . . . . . . 15
|
33 | | ssel 3497 |
. . . . . . . . . . . . . . 15
|
34 | 32, 33 | syl6 33 |
. . . . . . . . . . . . . 14
|
35 | 34 | ex 434 |
. . . . . . . . . . . . 13
|
36 | 35 | com3r 79 |
. . . . . . . . . . . 12
|
37 | 4, 36 | syld 44 |
. . . . . . . . . . 11
|
38 | 37 | com4r 86 |
. . . . . . . . . 10
|
39 | 38 | imp 429 |
. . . . . . . . 9
|
40 | 39 | exlimiv 1722 |
. . . . . . . 8
|
41 | 17, 40 | sylbi 195 |
. . . . . . 7
|
42 | 41 | com13 80 |
. . . . . 6
|
43 | 42 | imp 429 |
. . . . 5
|
44 | 12, 43 | sylancom 667 |
. . . 4
|
45 | 16, 44 | mtoi 178 |
. . 3
|
46 | 15 | onordi 4987 |
. . . 4
|
47 | | eloni 4893 |
. . . . 5
|
48 | 12, 47 | syl 16 |
. . . 4
|
49 | | ordtri4 4920 |
. . . 4
|
50 | 46, 48, 49 | sylancr 663 |
. . 3
|
51 | 14, 45, 50 | mpbir2and 922 |
. 2
|
52 | 51 | ex 434 |
1
|