Step | Hyp | Ref
| Expression |
1 | | brdomi 7966 |
. 2
|
2 | | simplr 792 |
. . . . . . . 8
AC
AC |
3 | | imassrn 5477 |
. . . . . . . . . . 11
|
4 | | simplll 798 |
. . . . . . . . . . . 12
AC
|
5 | | f1f 6101 |
. . . . . . . . . . . 12
|
6 | | frn 6053 |
. . . . . . . . . . . 12
|
7 | 4, 5, 6 | 3syl 18 |
. . . . . . . . . . 11
AC
|
8 | 3, 7 | syl5ss 3614 |
. . . . . . . . . 10
AC
|
9 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . 17
AC |
11 | 10 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
AC
|
12 | 11 | eldifad 3586 |
. . . . . . . . . . . . . . 15
AC
|
13 | 12 | elpwid 4170 |
. . . . . . . . . . . . . 14
AC
|
14 | | f1dm 6105 |
. . . . . . . . . . . . . . 15
|
15 | 4, 14 | syl 17 |
. . . . . . . . . . . . . 14
AC
|
16 | 13, 15 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
AC
|
17 | | sseqin2 3817 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | sylib 208 |
. . . . . . . . . . . 12
AC
|
19 | | eldifsni 4320 |
. . . . . . . . . . . . 13
|
20 | 11, 19 | syl 17 |
. . . . . . . . . . . 12
AC
|
21 | 18, 20 | eqnetrd 2861 |
. . . . . . . . . . 11
AC
|
22 | | imadisj 5484 |
. . . . . . . . . . . 12
|
23 | 22 | necon3bii 2846 |
. . . . . . . . . . 11
|
24 | 21, 23 | sylibr 224 |
. . . . . . . . . 10
AC
|
25 | 8, 24 | jca 554 |
. . . . . . . . 9
AC
|
26 | 25 | ralrimiva 2966 |
. . . . . . . 8
AC
|
27 | | acni2 8869 |
. . . . . . . 8
AC
|
28 | 2, 26, 27 | syl2anc 693 |
. . . . . . 7
AC
|
29 | | acnrcl 8865 |
. . . . . . . . 9
AC
|
30 | 29 | ad3antlr 767 |
. . . . . . . 8
AC |
31 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
AC
|
32 | | f1f1orn 6148 |
. . . . . . . . . . . . . . 15
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
AC
|
34 | | simprr 796 |
. . . . . . . . . . . . . . 15
AC
|
35 | 3, 34 | sseldi 3601 |
. . . . . . . . . . . . . 14
AC
|
36 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . . 14
|
37 | 33, 35, 36 | syl2anc 693 |
. . . . . . . . . . . . 13
AC
|
38 | 37, 34 | eqeltrd 2701 |
. . . . . . . . . . . 12
AC
|
39 | | f1ocnv 6149 |
. . . . . . . . . . . . . . 15
|
40 | | f1of 6137 |
. . . . . . . . . . . . . . 15
|
41 | 33, 39, 40 | 3syl 18 |
. . . . . . . . . . . . . 14
AC
|
42 | 41, 35 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
AC
|
43 | 13 | ad2ant2r 783 |
. . . . . . . . . . . . 13
AC
|
44 | | f1elima 6520 |
. . . . . . . . . . . . 13
|
45 | 31, 42, 43, 44 | syl3anc 1326 |
. . . . . . . . . . . 12
AC
|
46 | 38, 45 | mpbid 222 |
. . . . . . . . . . 11
AC
|
47 | 46 | expr 643 |
. . . . . . . . . 10
AC
|
48 | 47 | ralimdva 2962 |
. . . . . . . . 9
AC
|
49 | 48 | impr 649 |
. . . . . . . 8
AC
|
50 | | acnlem 8871 |
. . . . . . . 8
|
51 | 30, 49, 50 | syl2anc 693 |
. . . . . . 7
AC
|
52 | 28, 51 | exlimddv 1863 |
. . . . . 6
AC |
53 | 52 | ralrimiva 2966 |
. . . . 5
AC
|
54 | | vex 3203 |
. . . . . . . 8
|
55 | 54 | dmex 7099 |
. . . . . . 7
|
56 | 14, 55 | syl6eqelr 2710 |
. . . . . 6
|
57 | | isacn 8867 |
. . . . . 6
AC
|
58 | 56, 29, 57 | syl2an 494 |
. . . . 5
AC AC
|
59 | 53, 58 | mpbird 247 |
. . . 4
AC AC |
60 | 59 | ex 450 |
. . 3
AC
AC |
61 | 60 | exlimiv 1858 |
. 2
AC AC |
62 | 1, 61 | syl 17 |
1
AC
AC |