Step | Hyp | Ref
| Expression |
1 | | neq0 3930 |
. . . 4
|
2 | | ssel 3597 |
. . . . . . . . . . . . . 14
|
3 | | isof1o 6573 |
. . . . . . . . . . . . . . 15
|
4 | | f1ofn 6138 |
. . . . . . . . . . . . . . 15
|
5 | | fnbrfvb 6236 |
. . . . . . . . . . . . . . . 16
|
6 | 5 | ex 450 |
. . . . . . . . . . . . . . 15
|
7 | 3, 4, 6 | 3syl 18 |
. . . . . . . . . . . . . 14
|
8 | 2, 7 | syl9r 78 |
. . . . . . . . . . . . 13
|
9 | 8 | imp31 448 |
. . . . . . . . . . . 12
|
10 | 9 | rexbidva 3049 |
. . . . . . . . . . 11
|
11 | | vex 3203 |
. . . . . . . . . . . 12
|
12 | 11 | elima 5471 |
. . . . . . . . . . 11
|
13 | 10, 12 | syl6rbbr 279 |
. . . . . . . . . 10
|
14 | | fvex 6201 |
. . . . . . . . . . 11
|
15 | 11 | eliniseg 5494 |
. . . . . . . . . . 11
|
16 | 14, 15 | mp1i 13 |
. . . . . . . . . 10
|
17 | 13, 16 | anbi12d 747 |
. . . . . . . . 9
|
18 | | elin 3796 |
. . . . . . . . 9
|
19 | | r19.41v 3089 |
. . . . . . . . 9
|
20 | 17, 18, 19 | 3bitr4g 303 |
. . . . . . . 8
|
21 | 20 | adantrr 753 |
. . . . . . 7
|
22 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
23 | 22 | biimpar 502 |
. . . . . . . . . . . . 13
|
24 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
25 | 24 | eliniseg 5494 |
. . . . . . . . . . . . . . 15
|
26 | 25 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
27 | | isorel 6576 |
. . . . . . . . . . . . . 14
|
28 | 26, 27 | bitrd 268 |
. . . . . . . . . . . . 13
|
29 | 23, 28 | syl5ibr 236 |
. . . . . . . . . . . 12
|
30 | 29 | exp32 631 |
. . . . . . . . . . 11
|
31 | 2, 30 | syl9r 78 |
. . . . . . . . . 10
|
32 | 31 | com34 91 |
. . . . . . . . 9
|
33 | 32 | imp32 449 |
. . . . . . . 8
|
34 | 33 | reximdvai 3015 |
. . . . . . 7
|
35 | 21, 34 | sylbid 230 |
. . . . . 6
|
36 | | elin 3796 |
. . . . . . . 8
|
37 | 36 | exbii 1774 |
. . . . . . 7
|
38 | | neq0 3930 |
. . . . . . 7
|
39 | | df-rex 2918 |
. . . . . . 7
|
40 | 37, 38, 39 | 3bitr4i 292 |
. . . . . 6
|
41 | 35, 40 | syl6ibr 242 |
. . . . 5
|
42 | 41 | exlimdv 1861 |
. . . 4
|
43 | 1, 42 | syl5bi 232 |
. . 3
|
44 | 43 | con4d 114 |
. 2
|
45 | 3, 4 | syl 17 |
. . . . . . . . 9
|
46 | | fnfvima 6496 |
. . . . . . . . . . 11
|
47 | 46 | 3expia 1267 |
. . . . . . . . . 10
|
48 | 47 | adantrr 753 |
. . . . . . . . 9
|
49 | 45, 48 | sylan 488 |
. . . . . . . 8
|
50 | 49 | adantrd 484 |
. . . . . . 7
|
51 | 27 | biimpd 219 |
. . . . . . . . . . . . . 14
|
52 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | eliniseg 5494 |
. . . . . . . . . . . . . . 15
|
54 | 14, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
55 | 51, 54 | syl6ibr 242 |
. . . . . . . . . . . . 13
|
56 | 26, 55 | sylbid 230 |
. . . . . . . . . . . 12
|
57 | 56 | exp32 631 |
. . . . . . . . . . 11
|
58 | 2, 57 | syl9r 78 |
. . . . . . . . . 10
|
59 | 58 | com34 91 |
. . . . . . . . 9
|
60 | 59 | imp32 449 |
. . . . . . . 8
|
61 | 60 | impd 447 |
. . . . . . 7
|
62 | 50, 61 | jcad 555 |
. . . . . 6
|
63 | | elin 3796 |
. . . . . 6
|
64 | 62, 36, 63 | 3imtr4g 285 |
. . . . 5
|
65 | | n0i 3920 |
. . . . 5
|
66 | 64, 65 | syl6 35 |
. . . 4
|
67 | 66 | exlimdv 1861 |
. . 3
|
68 | 38, 67 | syl5bi 232 |
. 2
|
69 | 44, 68 | impcon4bid 217 |
1
|