Proof of Theorem uncf2
Step | Hyp | Ref
| Expression |
1 | | uncfval.g |
. . . . . . 7
uncurryF |
2 | | uncfval.c |
. . . . . . 7
|
3 | | uncfval.d |
. . . . . . 7
|
4 | | uncfval.f |
. . . . . . 7
FuncCat |
5 | 1, 2, 3, 4 | uncfval 16874 |
. . . . . 6
evalF func
func F
〈,〉F F |
6 | 5 | fveq2d 6195 |
. . . . 5
evalF
func func F
〈,〉F F
|
7 | 6 | oveqd 6667 |
. . . 4
evalF func
func F
〈,〉F F |
8 | 7 | oveqd 6667 |
. . 3
evalF func
func F
〈,〉F F |
9 | | df-ov 6653 |
. . . 4
evalF func
func F
〈,〉F F
evalF func
func F
〈,〉F F |
10 | | eqid 2622 |
. . . . . 6
c c |
11 | | uncf1.a |
. . . . . 6
|
12 | | uncf1.b |
. . . . . 6
|
13 | 10, 11, 12 | xpcbas 16818 |
. . . . 5
c |
14 | | eqid 2622 |
. . . . . 6
func F
〈,〉F F func F
〈,〉F F
|
15 | | eqid 2622 |
. . . . . 6
FuncCat c FuncCat c |
16 | | funcrcl 16523 |
. . . . . . . . . 10
FuncCat FuncCat
|
17 | 4, 16 | syl 17 |
. . . . . . . . 9
FuncCat
|
18 | 17 | simpld 475 |
. . . . . . . 8
|
19 | | eqid 2622 |
. . . . . . . 8
F F |
20 | 10, 18, 2, 19 | 1stfcl 16837 |
. . . . . . 7
F
c
|
21 | 20, 4 | cofucl 16548 |
. . . . . 6
func
F c FuncCat |
22 | | eqid 2622 |
. . . . . . 7
F F |
23 | 10, 18, 2, 22 | 2ndfcl 16838 |
. . . . . 6
F
c
|
24 | 14, 15, 21, 23 | prfcl 16843 |
. . . . 5
func F
〈,〉F F
c FuncCat
c |
25 | | eqid 2622 |
. . . . . 6
evalF evalF |
26 | | eqid 2622 |
. . . . . 6
FuncCat FuncCat |
27 | 25, 26, 2, 3 | evlfcl 16862 |
. . . . 5
evalF FuncCat c |
28 | | uncf1.x |
. . . . . 6
|
29 | | uncf1.y |
. . . . . 6
|
30 | | opelxpi 5148 |
. . . . . 6
|
31 | 28, 29, 30 | syl2anc 693 |
. . . . 5
|
32 | | uncf2.z |
. . . . . 6
|
33 | | uncf2.w |
. . . . . 6
|
34 | | opelxpi 5148 |
. . . . . 6
|
35 | 32, 33, 34 | syl2anc 693 |
. . . . 5
|
36 | | eqid 2622 |
. . . . 5
c c |
37 | | uncf2.r |
. . . . . . 7
|
38 | | uncf2.s |
. . . . . . 7
|
39 | | opelxpi 5148 |
. . . . . . 7
|
40 | 37, 38, 39 | syl2anc 693 |
. . . . . 6
|
41 | | uncf2.h |
. . . . . . 7
|
42 | | uncf2.j |
. . . . . . 7
|
43 | 10, 11, 12, 41, 42, 28, 29, 32, 33, 36 | xpchom2 16826 |
. . . . . 6
c
|
44 | 40, 43 | eleqtrrd 2704 |
. . . . 5
c
|
45 | 13, 24, 27, 31, 35, 36, 44 | cofu2 16546 |
. . . 4
evalF func
func F
〈,〉F F func F
〈,〉F F
evalF func F
〈,〉F F func
F
〈,〉F F
|
46 | 9, 45 | syl5eq 2668 |
. . 3
evalF func
func F
〈,〉F F func F
〈,〉F F evalF func F
〈,〉F F func
F
〈,〉F F
|
47 | 8, 46 | eqtrd 2656 |
. 2
func F
〈,〉F F
evalF func F
〈,〉F F func
F
〈,〉F F
|
48 | 14, 13, 36, 21, 23, 31 | prf1 16840 |
. . . . . 6
func
F
〈,〉F F
func
F F
|
49 | 13, 20, 4, 31 | cofu1 16544 |
. . . . . . . 8
func F
F |
50 | 10, 13, 36, 18, 2, 19, 31 | 1stf1 16832 |
. . . . . . . . . 10
F |
51 | | op1stg 7180 |
. . . . . . . . . . 11
|
52 | 28, 29, 51 | syl2anc 693 |
. . . . . . . . . 10
|
53 | 50, 52 | eqtrd 2656 |
. . . . . . . . 9
F |
54 | 53 | fveq2d 6195 |
. . . . . . . 8
F |
55 | 49, 54 | eqtrd 2656 |
. . . . . . 7
func F
|
56 | 10, 13, 36, 18, 2, 22, 31 | 2ndf1 16835 |
. . . . . . . 8
F |
57 | | op2ndg 7181 |
. . . . . . . . 9
|
58 | 28, 29, 57 | syl2anc 693 |
. . . . . . . 8
|
59 | 56, 58 | eqtrd 2656 |
. . . . . . 7
F |
60 | 55, 59 | opeq12d 4410 |
. . . . . 6
func F
F
|
61 | 48, 60 | eqtrd 2656 |
. . . . 5
func
F
〈,〉F F
|
62 | 14, 13, 36, 21, 23, 35 | prf1 16840 |
. . . . . 6
func
F
〈,〉F F
func
F F
|
63 | 13, 20, 4, 35 | cofu1 16544 |
. . . . . . . 8
func F
F |
64 | 10, 13, 36, 18, 2, 19, 35 | 1stf1 16832 |
. . . . . . . . . 10
F |
65 | | op1stg 7180 |
. . . . . . . . . . 11
|
66 | 32, 33, 65 | syl2anc 693 |
. . . . . . . . . 10
|
67 | 64, 66 | eqtrd 2656 |
. . . . . . . . 9
F |
68 | 67 | fveq2d 6195 |
. . . . . . . 8
F |
69 | 63, 68 | eqtrd 2656 |
. . . . . . 7
func F
|
70 | 10, 13, 36, 18, 2, 22, 35 | 2ndf1 16835 |
. . . . . . . 8
F |
71 | | op2ndg 7181 |
. . . . . . . . 9
|
72 | 32, 33, 71 | syl2anc 693 |
. . . . . . . 8
|
73 | 70, 72 | eqtrd 2656 |
. . . . . . 7
F |
74 | 69, 73 | opeq12d 4410 |
. . . . . 6
func F
F
|
75 | 62, 74 | eqtrd 2656 |
. . . . 5
func
F
〈,〉F F
|
76 | 61, 75 | oveq12d 6668 |
. . . 4
func F
〈,〉F F
evalF func F
〈,〉F F evalF |
77 | 14, 13, 36, 21, 23, 31, 35, 44 | prf2 16842 |
. . . . 5
func
F
〈,〉F F
func F
F
|
78 | 13, 20, 4, 31, 35, 36, 44 | cofu2 16546 |
. . . . . . 7
func F
F F
F
|
79 | 53, 67 | oveq12d 6668 |
. . . . . . . 8
F
F |
80 | 10, 13, 36, 18, 2, 19, 31, 35 | 1stf2 16833 |
. . . . . . . . . 10
F
c
|
81 | 80 | fveq1d 6193 |
. . . . . . . . 9
F
c |
82 | | fvres 6207 |
. . . . . . . . . 10
c
c
|
83 | 44, 82 | syl 17 |
. . . . . . . . 9
c
|
84 | | op1stg 7180 |
. . . . . . . . . 10
|
85 | 37, 38, 84 | syl2anc 693 |
. . . . . . . . 9
|
86 | 81, 83, 85 | 3eqtrd 2660 |
. . . . . . . 8
F
|
87 | 79, 86 | fveq12d 6197 |
. . . . . . 7
F F
F
|
88 | 78, 87 | eqtrd 2656 |
. . . . . 6
func F
|
89 | 10, 13, 36, 18, 2, 22, 31, 35 | 2ndf2 16836 |
. . . . . . . 8
F
c
|
90 | 89 | fveq1d 6193 |
. . . . . . 7
F
c |
91 | | fvres 6207 |
. . . . . . . 8
c
c
|
92 | 44, 91 | syl 17 |
. . . . . . 7
c
|
93 | | op2ndg 7181 |
. . . . . . . 8
|
94 | 37, 38, 93 | syl2anc 693 |
. . . . . . 7
|
95 | 90, 92, 94 | 3eqtrd 2660 |
. . . . . 6
F
|
96 | 88, 95 | opeq12d 4410 |
. . . . 5
func F
F
|
97 | 77, 96 | eqtrd 2656 |
. . . 4
func
F
〈,〉F F
|
98 | 76, 97 | fveq12d 6197 |
. . 3
func F
〈,〉F F evalF func F
〈,〉F F func
F
〈,〉F F
evalF |
99 | | df-ov 6653 |
. . 3
evalF evalF |
100 | 98, 99 | syl6eqr 2674 |
. 2
func F
〈,〉F F evalF func F
〈,〉F F func
F
〈,〉F F
evalF |
101 | | eqid 2622 |
. . 3
comp comp |
102 | | eqid 2622 |
. . 3
Nat Nat |
103 | 26 | fucbas 16620 |
. . . . 5
FuncCat |
104 | | relfunc 16522 |
. . . . . 6
FuncCat |
105 | | 1st2ndbr 7217 |
. . . . . 6
FuncCat
FuncCat
FuncCat |
106 | 104, 4, 105 | sylancr 695 |
. . . . 5
FuncCat |
107 | 11, 103, 106 | funcf1 16526 |
. . . 4
|
108 | 107, 28 | ffvelrnd 6360 |
. . 3
|
109 | 107, 32 | ffvelrnd 6360 |
. . 3
|
110 | | eqid 2622 |
. . 3
evalF evalF |
111 | 26, 102 | fuchom 16621 |
. . . . 5
Nat FuncCat |
112 | 11, 41, 111, 106, 28, 32 | funcf2 16528 |
. . . 4
Nat |
113 | 112, 37 | ffvelrnd 6360 |
. . 3
Nat |
114 | 25, 2, 3, 12, 42, 101, 102, 108, 109, 29, 33, 110, 113, 38 | evlf2val 16859 |
. 2
evalF comp |
115 | 47, 100, 114 | 3eqtrd 2660 |
1
comp |