Step | Hyp | Ref
| Expression |
1 | | eqid 2081 |
. . . . . . . . . . . . 13
recs recs |
2 | | frecsuclem1.h |
. . . . . . . . . . . . . 14
|
3 | 2 | frectfr 6008 |
. . . . . . . . . . . . 13
|
4 | 1, 3 | tfri1d 5972 |
. . . . . . . . . . . 12
recs |
5 | | fnfun 5016 |
. . . . . . . . . . . 12
recs recs |
6 | 4, 5 | syl 14 |
. . . . . . . . . . 11
recs |
7 | 6 | 3adant3 958 |
. . . . . . . . . 10
recs |
8 | | peano2 4336 |
. . . . . . . . . . 11
|
9 | 8 | 3ad2ant3 961 |
. . . . . . . . . 10
|
10 | | resfunexg 5403 |
. . . . . . . . . 10
recs recs |
11 | 7, 9, 10 | syl2anc 403 |
. . . . . . . . 9
recs
|
12 | | simp1 938 |
. . . . . . . . 9
|
13 | | simp2 939 |
. . . . . . . . 9
|
14 | 11, 12, 13 | frecabex 6007 |
. . . . . . . 8
recs
recs recs |
15 | | dmeq 4553 |
. . . . . . . . . . . . . . . . 17
recs
recs |
16 | 15 | eqeq1d 2089 |
. . . . . . . . . . . . . . . 16
recs
recs |
17 | | fveq1 5197 |
. . . . . . . . . . . . . . . . . 18
recs
recs |
18 | 17 | fveq2d 5202 |
. . . . . . . . . . . . . . . . 17
recs
recs |
19 | 18 | eleq2d 2148 |
. . . . . . . . . . . . . . . 16
recs
recs |
20 | 16, 19 | anbi12d 456 |
. . . . . . . . . . . . . . 15
recs
recs
recs |
21 | 20 | rexbidv 2369 |
. . . . . . . . . . . . . 14
recs
recs
recs |
22 | 15 | eqeq1d 2089 |
. . . . . . . . . . . . . . 15
recs
recs
|
23 | 22 | anbi1d 452 |
. . . . . . . . . . . . . 14
recs
recs |
24 | 21, 23 | orbi12d 739 |
. . . . . . . . . . . . 13
recs
recs recs recs |
25 | 24 | abbidv 2196 |
. . . . . . . . . . . 12
recs
recs
recs recs |
26 | 25, 2 | fvmptg 5269 |
. . . . . . . . . . 11
recs
recs
recs recs
recs
recs
recs recs |
27 | 26 | ex 113 |
. . . . . . . . . 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 6010 |
. . . . . . . . . 10
frec recs |
30 | 29 | eqeq1d 2089 |
. . . . . . . . 9
frec
recs
recs
recs
recs recs
recs recs |
31 | 28, 30 | sylibrd 167 |
. . . . . . . 8
recs
recs recs frec recs recs recs |
32 | 14, 31 | mpd 13 |
. . . . . . 7
frec recs recs recs |
33 | 32 | abeq2d 2191 |
. . . . . 6
frec recs
recs recs |
34 | 2 | frecsuclemdm 6011 |
. . . . . . . . . . 11
recs |
35 | | peano3 4337 |
. . . . . . . . . . . 12
|
36 | 35 | 3ad2ant3 961 |
. . . . . . . . . . 11
|
37 | 34, 36 | eqnetrd 2269 |
. . . . . . . . . 10
recs |
38 | 37 | neneqd 2266 |
. . . . . . . . 9
recs |
39 | 38 | intnanrd 874 |
. . . . . . . 8
recs |
40 | | biorf 695 |
. . . . . . . 8
recs
recs
recs
recs recs
recs |
41 | 39, 40 | syl 14 |
. . . . . . 7
recs
recs
recs recs
recs |
42 | | orcom 679 |
. . . . . . 7
recs
recs recs recs
recs recs |
43 | 41, 42 | syl6bb 194 |
. . . . . 6
recs
recs
recs recs recs |
44 | 34 | eqeq1d 2089 |
. . . . . . . . . 10
recs |
45 | | vex 2604 |
. . . . . . . . . . . 12
|
46 | | suc11g 4300 |
. . . . . . . . . . . 12
|
47 | 45, 46 | mpan2 415 |
. . . . . . . . . . 11
|
48 | 47 | 3ad2ant3 961 |
. . . . . . . . . 10
|
49 | 44, 48 | bitrd 186 |
. . . . . . . . 9
recs |
50 | | eqcom 2083 |
. . . . . . . . 9
|
51 | 49, 50 | syl6bb 194 |
. . . . . . . 8
recs |
52 | 51 | anbi1d 452 |
. . . . . . 7
recs recs recs |
53 | 52 | rexbidv 2369 |
. . . . . 6
recs
recs
recs |
54 | 33, 43, 53 | 3bitr2d 214 |
. . . . 5
frec
recs |
55 | | fveq2 5198 |
. . . . . . . 8
recs recs |
56 | 55 | fveq2d 5202 |
. . . . . . 7
recs recs |
57 | 56 | eleq2d 2148 |
. . . . . 6
recs
recs |
58 | 57 | ceqsrexbv 2726 |
. . . . 5
recs
recs |
59 | 54, 58 | syl6bb 194 |
. . . 4
frec
recs |
60 | 59 | 3anibar 1106 |
. . 3
frec
recs |
61 | 60 | eqrdv 2079 |
. 2
frec recs |
62 | 2 | frecsuclem2 6012 |
. . 3
recs frec |
63 | 62 | fveq2d 5202 |
. 2
recs frec |
64 | 61, 63 | eqtrd 2113 |
1
frec frec |