Step | Hyp | Ref
| Expression |
1 | | ineq2 3808 |
. . . . . . . 8
|
2 | 1 | eleq2d 2687 |
. . . . . . 7
|
3 | 2 | eubidv 2490 |
. . . . . 6
|
4 | 3 | imbi2d 330 |
. . . . 5
|
5 | 4 | ralbidv 2986 |
. . . 4
|
6 | 5 | cbvexv 2275 |
. . 3
|
7 | | indi 3873 |
. . . . . . . . . . . 12
|
8 | | elssuni 4467 |
. . . . . . . . . . . . . . . . 17
|
9 | 8 | ssneld 3605 |
. . . . . . . . . . . . . . . 16
|
10 | | disjsn 4246 |
. . . . . . . . . . . . . . . 16
|
11 | 9, 10 | syl6ibr 242 |
. . . . . . . . . . . . . . 15
|
12 | 11 | impcom 446 |
. . . . . . . . . . . . . 14
|
13 | 12 | uneq2d 3767 |
. . . . . . . . . . . . 13
|
14 | | un0 3967 |
. . . . . . . . . . . . 13
|
15 | 13, 14 | syl6eq 2672 |
. . . . . . . . . . . 12
|
16 | 7, 15 | syl5req 2669 |
. . . . . . . . . . 11
|
17 | 16 | eleq2d 2687 |
. . . . . . . . . 10
|
18 | 17 | eubidv 2490 |
. . . . . . . . 9
|
19 | 18 | imbi2d 330 |
. . . . . . . 8
|
20 | 19 | ralbidva 2985 |
. . . . . . 7
|
21 | | vsnid 4209 |
. . . . . . . . . . . 12
|
22 | 21 | olci 406 |
. . . . . . . . . . 11
|
23 | | elun 3753 |
. . . . . . . . . . 11
|
24 | 22, 23 | mpbir 221 |
. . . . . . . . . 10
|
25 | | elssuni 4467 |
. . . . . . . . . . 11
|
26 | 25 | sseld 3602 |
. . . . . . . . . 10
|
27 | 24, 26 | mpi 20 |
. . . . . . . . 9
|
28 | 27 | con3i 150 |
. . . . . . . 8
|
29 | 28 | biantrurd 529 |
. . . . . . 7
|
30 | 20, 29 | bitrd 268 |
. . . . . 6
|
31 | | vex 3203 |
. . . . . . . 8
|
32 | | snex 4908 |
. . . . . . . 8
|
33 | 31, 32 | unex 6956 |
. . . . . . 7
|
34 | | eleq1 2689 |
. . . . . . . . 9
|
35 | 34 | notbid 308 |
. . . . . . . 8
|
36 | | ineq2 3808 |
. . . . . . . . . . . 12
|
37 | 36 | eleq2d 2687 |
. . . . . . . . . . 11
|
38 | 37 | eubidv 2490 |
. . . . . . . . . 10
|
39 | 38 | imbi2d 330 |
. . . . . . . . 9
|
40 | 39 | ralbidv 2986 |
. . . . . . . 8
|
41 | 35, 40 | anbi12d 747 |
. . . . . . 7
|
42 | 33, 41 | spcev 3300 |
. . . . . 6
|
43 | 30, 42 | syl6bi 243 |
. . . . 5
|
44 | | vuniex 6954 |
. . . . . 6
|
45 | | eleq2 2690 |
. . . . . . . 8
|
46 | 45 | notbid 308 |
. . . . . . 7
|
47 | 46 | exbidv 1850 |
. . . . . 6
|
48 | | nalset 4795 |
. . . . . . . 8
|
49 | | alexn 1771 |
. . . . . . . 8
|
50 | 48, 49 | mpbir 221 |
. . . . . . 7
|
51 | 50 | spi 2054 |
. . . . . 6
|
52 | 44, 47, 51 | vtocl 3259 |
. . . . 5
|
53 | 43, 52 | exlimiiv 1859 |
. . . 4
|
54 | 53 | exlimiv 1858 |
. . 3
|
55 | 6, 54 | sylbi 207 |
. 2
|
56 | | exsimpr 1796 |
. 2
|
57 | 55, 56 | impbii 199 |
1
|