Step | Hyp | Ref
| Expression |
1 | | sucelon 7017 |
. . 3
|
2 | | cfval 9069 |
. . 3
|
3 | 1, 2 | sylbi 207 |
. 2
|
4 | | cardsn 8795 |
. . . . . 6
|
5 | 4 | eqcomd 2628 |
. . . . 5
|
6 | | snidg 4206 |
. . . . . . . 8
|
7 | | elsuci 5791 |
. . . . . . . . 9
|
8 | | onelss 5766 |
. . . . . . . . . 10
|
9 | | eqimss 3657 |
. . . . . . . . . . 11
|
10 | 9 | a1i 11 |
. . . . . . . . . 10
|
11 | 8, 10 | jaod 395 |
. . . . . . . . 9
|
12 | 7, 11 | syl5 34 |
. . . . . . . 8
|
13 | | sseq2 3627 |
. . . . . . . . 9
|
14 | 13 | rspcev 3309 |
. . . . . . . 8
|
15 | 6, 12, 14 | syl6an 568 |
. . . . . . 7
|
16 | 15 | ralrimiv 2965 |
. . . . . 6
|
17 | | ssun2 3777 |
. . . . . . 7
|
18 | | df-suc 5729 |
. . . . . . 7
|
19 | 17, 18 | sseqtr4i 3638 |
. . . . . 6
|
20 | 16, 19 | jctil 560 |
. . . . 5
|
21 | | snex 4908 |
. . . . . 6
|
22 | | fveq2 6191 |
. . . . . . . 8
|
23 | 22 | eqeq2d 2632 |
. . . . . . 7
|
24 | | sseq1 3626 |
. . . . . . . 8
|
25 | | rexeq 3139 |
. . . . . . . . 9
|
26 | 25 | ralbidv 2986 |
. . . . . . . 8
|
27 | 24, 26 | anbi12d 747 |
. . . . . . 7
|
28 | 23, 27 | anbi12d 747 |
. . . . . 6
|
29 | 21, 28 | spcev 3300 |
. . . . 5
|
30 | 5, 20, 29 | syl2anc 693 |
. . . 4
|
31 | | 1on 7567 |
. . . . . 6
|
32 | 31 | elexi 3213 |
. . . . 5
|
33 | | eqeq1 2626 |
. . . . . . 7
|
34 | 33 | anbi1d 741 |
. . . . . 6
|
35 | 34 | exbidv 1850 |
. . . . 5
|
36 | 32, 35 | elab 3350 |
. . . 4
|
37 | 30, 36 | sylibr 224 |
. . 3
|
38 | | el1o 7579 |
. . . . 5
|
39 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
|
40 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
41 | | onssnum 8863 |
. . . . . . . . . . . . . . . . 17
|
42 | 40, 41 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
43 | | cardnueq0 8790 |
. . . . . . . . . . . . . . . 16
|
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . 15
|
45 | 39, 44 | syl5bb 272 |
. . . . . . . . . . . . . 14
|
46 | 45 | biimpa 501 |
. . . . . . . . . . . . 13
|
47 | | rex0 3938 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | nrex 3000 |
. . . . . . . . . . . . . . 15
|
50 | | nsuceq0 5805 |
. . . . . . . . . . . . . . . 16
|
51 | | r19.2z 4060 |
. . . . . . . . . . . . . . . 16
|
52 | 50, 51 | mpan 706 |
. . . . . . . . . . . . . . 15
|
53 | 49, 52 | mto 188 |
. . . . . . . . . . . . . 14
|
54 | | rexeq 3139 |
. . . . . . . . . . . . . . 15
|
55 | 54 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
56 | 53, 55 | mtbiri 317 |
. . . . . . . . . . . . 13
|
57 | 46, 56 | syl 17 |
. . . . . . . . . . . 12
|
58 | 57 | intnand 962 |
. . . . . . . . . . 11
|
59 | | imnan 438 |
. . . . . . . . . . 11
|
60 | 58, 59 | mpbi 220 |
. . . . . . . . . 10
|
61 | | suceloni 7013 |
. . . . . . . . . . . . . . . 16
|
62 | | onss 6990 |
. . . . . . . . . . . . . . . . 17
|
63 | | sstr 3611 |
. . . . . . . . . . . . . . . . 17
|
64 | 62, 63 | sylan2 491 |
. . . . . . . . . . . . . . . 16
|
65 | 61, 64 | sylan2 491 |
. . . . . . . . . . . . . . 15
|
66 | 65 | ancoms 469 |
. . . . . . . . . . . . . 14
|
67 | 66 | adantrr 753 |
. . . . . . . . . . . . 13
|
68 | 67 | 3adant2 1080 |
. . . . . . . . . . . 12
|
69 | | simp2 1062 |
. . . . . . . . . . . 12
|
70 | | simp3 1063 |
. . . . . . . . . . . 12
|
71 | 68, 69, 70 | jca31 557 |
. . . . . . . . . . 11
|
72 | 71 | 3expib 1268 |
. . . . . . . . . 10
|
73 | 60, 72 | mtoi 190 |
. . . . . . . . 9
|
74 | 73 | nexdv 1864 |
. . . . . . . 8
|
75 | | 0ex 4790 |
. . . . . . . . 9
|
76 | | eqeq1 2626 |
. . . . . . . . . . 11
|
77 | 76 | anbi1d 741 |
. . . . . . . . . 10
|
78 | 77 | exbidv 1850 |
. . . . . . . . 9
|
79 | 75, 78 | elab 3350 |
. . . . . . . 8
|
80 | 74, 79 | sylnibr 319 |
. . . . . . 7
|
81 | 80 | adantr 481 |
. . . . . 6
|
82 | | eleq1 2689 |
. . . . . . 7
|
83 | 82 | adantl 482 |
. . . . . 6
|
84 | 81, 83 | mtbird 315 |
. . . . 5
|
85 | 38, 84 | sylan2b 492 |
. . . 4
|
86 | 85 | ralrimiva 2966 |
. . 3
|
87 | | cardon 8770 |
. . . . . . . 8
|
88 | | eleq1 2689 |
. . . . . . . 8
|
89 | 87, 88 | mpbiri 248 |
. . . . . . 7
|
90 | 89 | adantr 481 |
. . . . . 6
|
91 | 90 | exlimiv 1858 |
. . . . 5
|
92 | 91 | abssi 3677 |
. . . 4
|
93 | | oneqmini 5776 |
. . . 4
|
94 | 92, 93 | ax-mp 5 |
. . 3
|
95 | 37, 86, 94 | syl2anc 693 |
. 2
|
96 | 3, 95 | eqtr4d 2659 |
1
|