Step | Hyp | Ref
| Expression |
1 | | eqid 2040 |
. . . . . . . . . . . . 13
recs recs |
2 | | frecsuclem1.h |
. . . . . . . . . . . . . 14
|
3 | 2 | frectfr 5985 |
. . . . . . . . . . . . 13
|
4 | 1, 3 | tfri1d 5949 |
. . . . . . . . . . . 12
recs |
5 | | fnfun 4996 |
. . . . . . . . . . . 12
recs recs |
6 | 4, 5 | syl 14 |
. . . . . . . . . . 11
recs |
7 | 6 | 3adant3 924 |
. . . . . . . . . 10
recs |
8 | | peano2 4318 |
. . . . . . . . . . 11
|
9 | 8 | 3ad2ant3 927 |
. . . . . . . . . 10
|
10 | | resfunexg 5382 |
. . . . . . . . . 10
recs recs |
11 | 7, 9, 10 | syl2anc 391 |
. . . . . . . . 9
recs
|
12 | | simp1 904 |
. . . . . . . . 9
|
13 | | simp2 905 |
. . . . . . . . 9
|
14 | 11, 12, 13 | frecabex 5984 |
. . . . . . . 8
recs
recs recs |
15 | | dmeq 4535 |
. . . . . . . . . . . . . . . . 17
recs
recs |
16 | 15 | eqeq1d 2048 |
. . . . . . . . . . . . . . . 16
recs
recs |
17 | | fveq1 5177 |
. . . . . . . . . . . . . . . . . 18
recs
recs |
18 | 17 | fveq2d 5182 |
. . . . . . . . . . . . . . . . 17
recs
recs |
19 | 18 | eleq2d 2107 |
. . . . . . . . . . . . . . . 16
recs
recs |
20 | 16, 19 | anbi12d 442 |
. . . . . . . . . . . . . . 15
recs
recs
recs |
21 | 20 | rexbidv 2327 |
. . . . . . . . . . . . . 14
recs
recs
recs |
22 | 15 | eqeq1d 2048 |
. . . . . . . . . . . . . . 15
recs
recs
|
23 | 22 | anbi1d 438 |
. . . . . . . . . . . . . 14
recs
recs |
24 | 21, 23 | orbi12d 707 |
. . . . . . . . . . . . 13
recs
recs recs recs |
25 | 24 | abbidv 2155 |
. . . . . . . . . . . 12
recs
recs
recs recs |
26 | 25, 2 | fvmptg 5248 |
. . . . . . . . . . 11
recs
recs
recs recs
recs
recs
recs recs |
27 | 26 | ex 108 |
. . . . . . . . . 10
recs recs
recs recs recs recs
recs
recs |
28 | 11, 27 | syl 14 |
. . . . . . . . 9
recs
recs recs recs recs
recs
recs |
29 | 2 | frecsuclem1 5987 |
. . . . . . . . . 10
frec recs |
30 | 29 | eqeq1d 2048 |
. . . . . . . . 9
frec
recs
recs
recs
recs recs
recs recs |
31 | 28, 30 | sylibrd 158 |
. . . . . . . 8
recs
recs recs frec recs recs recs |
32 | 14, 31 | mpd 13 |
. . . . . . 7
frec recs recs recs |
33 | 32 | abeq2d 2150 |
. . . . . 6
frec recs
recs recs |
34 | 2 | frecsuclemdm 5988 |
. . . . . . . . . . 11
recs |
35 | | peano3 4319 |
. . . . . . . . . . . 12
|
36 | 35 | 3ad2ant3 927 |
. . . . . . . . . . 11
|
37 | 34, 36 | eqnetrd 2229 |
. . . . . . . . . 10
recs |
38 | 37 | neneqd 2226 |
. . . . . . . . 9
recs |
39 | 38 | intnanrd 841 |
. . . . . . . 8
recs |
40 | | biorf 663 |
. . . . . . . 8
recs
recs
recs
recs recs
recs |
41 | 39, 40 | syl 14 |
. . . . . . 7
recs
recs
recs recs
recs |
42 | | orcom 647 |
. . . . . . 7
recs
recs recs recs
recs recs |
43 | 41, 42 | syl6bb 185 |
. . . . . 6
recs
recs
recs recs recs |
44 | 34 | eqeq1d 2048 |
. . . . . . . . . 10
recs |
45 | | vex 2560 |
. . . . . . . . . . . 12
|
46 | | suc11g 4281 |
. . . . . . . . . . . 12
|
47 | 45, 46 | mpan2 401 |
. . . . . . . . . . 11
|
48 | 47 | 3ad2ant3 927 |
. . . . . . . . . 10
|
49 | 44, 48 | bitrd 177 |
. . . . . . . . 9
recs |
50 | | eqcom 2042 |
. . . . . . . . 9
|
51 | 49, 50 | syl6bb 185 |
. . . . . . . 8
recs |
52 | 51 | anbi1d 438 |
. . . . . . 7
recs recs recs |
53 | 52 | rexbidv 2327 |
. . . . . 6
recs
recs
recs |
54 | 33, 43, 53 | 3bitr2d 205 |
. . . . 5
frec
recs |
55 | | fveq2 5178 |
. . . . . . . 8
recs recs |
56 | 55 | fveq2d 5182 |
. . . . . . 7
recs recs |
57 | 56 | eleq2d 2107 |
. . . . . 6
recs
recs |
58 | 57 | ceqsrexbv 2675 |
. . . . 5
recs
recs |
59 | 54, 58 | syl6bb 185 |
. . . 4
frec
recs |
60 | 59 | 3anibar 1072 |
. . 3
frec
recs |
61 | 60 | eqrdv 2038 |
. 2
frec recs |
62 | 2 | frecsuclem2 5989 |
. . 3
recs frec |
63 | 62 | fveq2d 5182 |
. 2
recs frec |
64 | 61, 63 | eqtrd 2072 |
1
frec frec |