Step | Hyp | Ref
| Expression |
1 | | frfnom 7530 |
. . . . . . . 8
|
2 | | axdclem2.1 |
. . . . . . . . 9
|
3 | 2 | fneq1i 5985 |
. . . . . . . 8
|
4 | 1, 3 | mpbir 221 |
. . . . . . 7
|
5 | 4 | a1i 11 |
. . . . . 6
|
6 | | fveq2 6191 |
. . . . . . . . . . 11
|
7 | | suceq 5790 |
. . . . . . . . . . . 12
|
8 | 7 | fveq2d 6195 |
. . . . . . . . . . 11
|
9 | 6, 8 | breq12d 4666 |
. . . . . . . . . 10
|
10 | | fveq2 6191 |
. . . . . . . . . . 11
|
11 | | suceq 5790 |
. . . . . . . . . . . 12
|
12 | 11 | fveq2d 6195 |
. . . . . . . . . . 11
|
13 | 10, 12 | breq12d 4666 |
. . . . . . . . . 10
|
14 | | fveq2 6191 |
. . . . . . . . . . 11
|
15 | | suceq 5790 |
. . . . . . . . . . . 12
|
16 | 15 | fveq2d 6195 |
. . . . . . . . . . 11
|
17 | 14, 16 | breq12d 4666 |
. . . . . . . . . 10
|
18 | 2 | fveq1i 6192 |
. . . . . . . . . . . . . . . 16
|
19 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
20 | | fr0g 7531 |
. . . . . . . . . . . . . . . . 17
|
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
22 | 18, 21 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
23 | 22 | breq1i 4660 |
. . . . . . . . . . . . . 14
|
24 | 23 | biimpri 218 |
. . . . . . . . . . . . 13
|
25 | 24 | eximi 1762 |
. . . . . . . . . . . 12
|
26 | | peano1 7085 |
. . . . . . . . . . . . 13
|
27 | 2 | axdclem 9341 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | mpi 20 |
. . . . . . . . . . . 12
|
29 | 25, 28 | syl3an3 1361 |
. . . . . . . . . . 11
|
30 | 29 | 3com23 1271 |
. . . . . . . . . 10
|
31 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
32 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
33 | 31, 32 | brelrn 5356 |
. . . . . . . . . . . . . . . 16
|
34 | | ssel 3597 |
. . . . . . . . . . . . . . . 16
|
35 | 33, 34 | syl5 34 |
. . . . . . . . . . . . . . 15
|
36 | 32 | eldm 5321 |
. . . . . . . . . . . . . . 15
|
37 | 35, 36 | syl6ib 241 |
. . . . . . . . . . . . . 14
|
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . 13
|
39 | | peano2 7086 |
. . . . . . . . . . . . . . . . 17
|
40 | 2 | axdclem 9341 |
. . . . . . . . . . . . . . . . 17
|
41 | 39, 40 | syl5 34 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | 3expia 1267 |
. . . . . . . . . . . . . . 15
|
43 | 42 | com3r 87 |
. . . . . . . . . . . . . 14
|
44 | 43 | imp 445 |
. . . . . . . . . . . . 13
|
45 | 38, 44 | syld 47 |
. . . . . . . . . . . 12
|
46 | 45 | 3adantr2 1221 |
. . . . . . . . . . 11
|
47 | 46 | ex 450 |
. . . . . . . . . 10
|
48 | 9, 13, 17, 30, 47 | finds2 7094 |
. . . . . . . . 9
|
49 | 48 | com12 32 |
. . . . . . . 8
|
50 | | fvex 6201 |
. . . . . . . . 9
|
51 | | fvex 6201 |
. . . . . . . . 9
|
52 | 50, 51 | breldm 5329 |
. . . . . . . 8
|
53 | 49, 52 | syl6 35 |
. . . . . . 7
|
54 | 53 | ralrimiv 2965 |
. . . . . 6
|
55 | | ffnfv 6388 |
. . . . . 6
|
56 | 5, 54, 55 | sylanbrc 698 |
. . . . 5
|
57 | | omex 8540 |
. . . . . 6
|
58 | 57 | a1i 11 |
. . . . 5
|
59 | | vex 3203 |
. . . . . . 7
|
60 | 59 | dmex 7099 |
. . . . . 6
|
61 | 60 | a1i 11 |
. . . . 5
|
62 | | fex2 7121 |
. . . . 5
|
63 | 56, 58, 61, 62 | syl3anc 1326 |
. . . 4
|
64 | 49 | ralrimiv 2965 |
. . . 4
|
65 | | fveq1 6190 |
. . . . . . 7
|
66 | | fveq1 6190 |
. . . . . . 7
|
67 | 65, 66 | breq12d 4666 |
. . . . . 6
|
68 | 67 | ralbidv 2986 |
. . . . 5
|
69 | 68 | spcegv 3294 |
. . . 4
|
70 | 63, 64, 69 | sylc 65 |
. . 3
|
71 | 70 | 3exp 1264 |
. 2
|
72 | 60 | pwex 4848 |
. . 3
|
73 | 72 | ac4c 9298 |
. 2
|
74 | 71, 73 | exlimiiv 1859 |
1
|