Step | Hyp | Ref
| Expression |
1 | | fuccocl.q |
. . . 4
FuncCat
|
2 | | fuccocl.n |
. . . 4
Nat |
3 | | eqid 2622 |
. . . 4
|
4 | | eqid 2622 |
. . . 4
comp comp |
5 | | fuccocl.x |
. . . 4
comp |
6 | | fuccocl.r |
. . . 4
|
7 | | fuccocl.s |
. . . 4
|
8 | 1, 2, 3, 4, 5, 6, 7 | fucco 16622 |
. . 3
comp |
9 | | eqid 2622 |
. . . . . 6
|
10 | | eqid 2622 |
. . . . . 6
|
11 | 2 | natrcl 16610 |
. . . . . . . . . . 11
|
12 | 6, 11 | syl 17 |
. . . . . . . . . 10
|
13 | 12 | simpld 475 |
. . . . . . . . 9
|
14 | | funcrcl 16523 |
. . . . . . . . 9
|
15 | 13, 14 | syl 17 |
. . . . . . . 8
|
16 | 15 | simprd 479 |
. . . . . . 7
|
17 | 16 | adantr 481 |
. . . . . 6
|
18 | | relfunc 16522 |
. . . . . . . . 9
|
19 | | 1st2ndbr 7217 |
. . . . . . . . 9
|
20 | 18, 13, 19 | sylancr 695 |
. . . . . . . 8
|
21 | 3, 9, 20 | funcf1 16526 |
. . . . . . 7
|
22 | 21 | ffvelrnda 6359 |
. . . . . 6
|
23 | 2 | natrcl 16610 |
. . . . . . . . . . 11
|
24 | 7, 23 | syl 17 |
. . . . . . . . . 10
|
25 | 24 | simpld 475 |
. . . . . . . . 9
|
26 | | 1st2ndbr 7217 |
. . . . . . . . 9
|
27 | 18, 25, 26 | sylancr 695 |
. . . . . . . 8
|
28 | 3, 9, 27 | funcf1 16526 |
. . . . . . 7
|
29 | 28 | ffvelrnda 6359 |
. . . . . 6
|
30 | 24 | simprd 479 |
. . . . . . . . 9
|
31 | | 1st2ndbr 7217 |
. . . . . . . . 9
|
32 | 18, 30, 31 | sylancr 695 |
. . . . . . . 8
|
33 | 3, 9, 32 | funcf1 16526 |
. . . . . . 7
|
34 | 33 | ffvelrnda 6359 |
. . . . . 6
|
35 | 2, 6 | nat1st2nd 16611 |
. . . . . . . 8
|
36 | 35 | adantr 481 |
. . . . . . 7
|
37 | | simpr 477 |
. . . . . . 7
|
38 | 2, 36, 3, 10, 37 | natcl 16613 |
. . . . . 6
|
39 | 2, 7 | nat1st2nd 16611 |
. . . . . . . 8
|
40 | 39 | adantr 481 |
. . . . . . 7
|
41 | 2, 40, 3, 10, 37 | natcl 16613 |
. . . . . 6
|
42 | 9, 10, 4, 17, 22, 29, 34, 38, 41 | catcocl 16346 |
. . . . 5
comp |
43 | 42 | ralrimiva 2966 |
. . . 4
comp |
44 | | fvex 6201 |
. . . . 5
|
45 | | mptelixpg 7945 |
. . . . 5
comp
comp |
46 | 44, 45 | ax-mp 5 |
. . . 4
comp
comp |
47 | 43, 46 | sylibr 224 |
. . 3
comp |
48 | 8, 47 | eqeltrd 2701 |
. 2
|
49 | 16 | adantr 481 |
. . . . . 6
|
50 | 21 | adantr 481 |
. . . . . . 7
|
51 | | simpr1 1067 |
. . . . . . 7
|
52 | 50, 51 | ffvelrnd 6360 |
. . . . . 6
|
53 | | simpr2 1068 |
. . . . . . 7
|
54 | 50, 53 | ffvelrnd 6360 |
. . . . . 6
|
55 | 28 | adantr 481 |
. . . . . . 7
|
56 | 55, 53 | ffvelrnd 6360 |
. . . . . 6
|
57 | | eqid 2622 |
. . . . . . . 8
|
58 | 20 | adantr 481 |
. . . . . . . 8
|
59 | 3, 57, 10, 58, 51, 53 | funcf2 16528 |
. . . . . . 7
|
60 | | simpr3 1069 |
. . . . . . 7
|
61 | 59, 60 | ffvelrnd 6360 |
. . . . . 6
|
62 | 35 | adantr 481 |
. . . . . . 7
|
63 | 2, 62, 3, 10, 53 | natcl 16613 |
. . . . . 6
|
64 | 33 | adantr 481 |
. . . . . . 7
|
65 | 64, 53 | ffvelrnd 6360 |
. . . . . 6
|
66 | 39 | adantr 481 |
. . . . . . 7
|
67 | 2, 66, 3, 10, 53 | natcl 16613 |
. . . . . 6
|
68 | 9, 10, 4, 49, 52, 54, 56, 61, 63, 65, 67 | catass 16347 |
. . . . 5
comp comp comp comp |
69 | 2, 62, 3, 57, 4, 51, 53, 60 | nati 16615 |
. . . . . . 7
comp comp |
70 | 69 | oveq2d 6666 |
. . . . . 6
comp comp comp comp |
71 | 55, 51 | ffvelrnd 6360 |
. . . . . . 7
|
72 | 2, 62, 3, 10, 51 | natcl 16613 |
. . . . . . 7
|
73 | 27 | adantr 481 |
. . . . . . . . 9
|
74 | 3, 57, 10, 73, 51, 53 | funcf2 16528 |
. . . . . . . 8
|
75 | 74, 60 | ffvelrnd 6360 |
. . . . . . 7
|
76 | 9, 10, 4, 49, 52, 71, 56, 72, 75, 65, 67 | catass 16347 |
. . . . . 6
comp comp comp comp |
77 | 2, 66, 3, 57, 4, 51, 53, 60 | nati 16615 |
. . . . . . 7
comp comp |
78 | 77 | oveq1d 6665 |
. . . . . 6
comp comp comp comp |
79 | 70, 76, 78 | 3eqtr2d 2662 |
. . . . 5
comp comp comp comp |
80 | 64, 51 | ffvelrnd 6360 |
. . . . . 6
|
81 | 2, 66, 3, 10, 51 | natcl 16613 |
. . . . . 6
|
82 | 32 | adantr 481 |
. . . . . . . 8
|
83 | 3, 57, 10, 82, 51, 53 | funcf2 16528 |
. . . . . . 7
|
84 | 83, 60 | ffvelrnd 6360 |
. . . . . 6
|
85 | 9, 10, 4, 49, 52, 71, 80, 72, 81, 65, 84 | catass 16347 |
. . . . 5
comp comp comp comp |
86 | 68, 79, 85 | 3eqtrd 2660 |
. . . 4
comp comp comp comp |
87 | 6 | adantr 481 |
. . . . . 6
|
88 | 7 | adantr 481 |
. . . . . 6
|
89 | 1, 2, 3, 4, 5, 87,
88, 53 | fuccoval 16623 |
. . . . 5
comp |
90 | 89 | oveq1d 6665 |
. . . 4
comp comp comp |
91 | 1, 2, 3, 4, 5, 87,
88, 51 | fuccoval 16623 |
. . . . 5
comp |
92 | 91 | oveq2d 6666 |
. . . 4
comp comp comp |
93 | 86, 90, 92 | 3eqtr4d 2666 |
. . 3
comp comp |
94 | 93 | ralrimivvva 2972 |
. 2
comp comp |
95 | 2, 3, 57, 10, 4, 13, 30 | isnat2 16608 |
. 2
comp comp |
96 | 48, 94, 95 | mpbir2and 957 |
1
|