Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . . . 10
|
2 | | id 22 |
. . . . . . . . . 10
|
3 | 1, 2 | eqeq12d 2637 |
. . . . . . . . 9
|
4 | 3 | rspcv 3305 |
. . . . . . . 8
|
5 | | cardon 8770 |
. . . . . . . . 9
|
6 | | eleq1 2689 |
. . . . . . . . 9
|
7 | 5, 6 | mpbii 223 |
. . . . . . . 8
|
8 | 4, 7 | syl6com 37 |
. . . . . . 7
|
9 | 8 | ssrdv 3609 |
. . . . . 6
|
10 | | ssonuni 6986 |
. . . . . 6
|
11 | 9, 10 | syl5 34 |
. . . . 5
|
12 | 11 | imp 445 |
. . . 4
|
13 | | cardonle 8783 |
. . . 4
|
14 | 12, 13 | syl 17 |
. . 3
|
15 | | cardon 8770 |
. . . . 5
|
16 | 15 | onirri 5834 |
. . . 4
|
17 | | eluni 4439 |
. . . . . . . 8
|
18 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . 18
|
19 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
21 | 18, 20 | syl5 34 |
. . . . . . . . . . . . . . . . 17
|
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
23 | | onenon 8775 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
25 | 22, 24 | syl6eqelr 2710 |
. . . . . . . . . . . . . . . . . 18
|
26 | | onenon 8775 |
. . . . . . . . . . . . . . . . . 18
|
27 | | carddom2 8803 |
. . . . . . . . . . . . . . . . . 18
|
28 | 25, 26, 27 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
29 | 21, 28 | sylibrd 249 |
. . . . . . . . . . . . . . . 16
|
30 | | sseq1 3626 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
32 | 29, 31 | sylibd 229 |
. . . . . . . . . . . . . . 15
|
33 | | ssel 3597 |
. . . . . . . . . . . . . . 15
|
34 | 32, 33 | syl6 35 |
. . . . . . . . . . . . . 14
|
35 | 34 | ex 450 |
. . . . . . . . . . . . 13
|
36 | 35 | com3r 87 |
. . . . . . . . . . . 12
|
37 | 4, 36 | syld 47 |
. . . . . . . . . . 11
|
38 | 37 | com4r 94 |
. . . . . . . . . 10
|
39 | 38 | imp 445 |
. . . . . . . . 9
|
40 | 39 | exlimiv 1858 |
. . . . . . . 8
|
41 | 17, 40 | sylbi 207 |
. . . . . . 7
|
42 | 41 | com13 88 |
. . . . . 6
|
43 | 42 | imp 445 |
. . . . 5
|
44 | 12, 43 | sylancom 701 |
. . . 4
|
45 | 16, 44 | mtoi 190 |
. . 3
|
46 | 15 | onordi 5832 |
. . . 4
|
47 | | eloni 5733 |
. . . . 5
|
48 | 12, 47 | syl 17 |
. . . 4
|
49 | | ordtri4 5761 |
. . . 4
|
50 | 46, 48, 49 | sylancr 695 |
. . 3
|
51 | 14, 45, 50 | mpbir2and 957 |
. 2
|
52 | 51 | ex 450 |
1
|