Step | Hyp | Ref
| Expression |
1 | | funcres.f |
. . . 4
|
2 | | funcres.h |
. . . 4
Subcat |
3 | 1, 2 | resfval 16552 |
. . 3
f |
4 | 3 | fveq2d 6195 |
. . . . 5
f |
5 | | fvex 6201 |
. . . . . . 7
|
6 | 5 | resex 5443 |
. . . . . 6
|
7 | | dmexg 7097 |
. . . . . . 7
Subcat
|
8 | | mptexg 6484 |
. . . . . . 7
|
9 | 2, 7, 8 | 3syl 18 |
. . . . . 6
|
10 | | op2ndg 7181 |
. . . . . 6
|
11 | 6, 9, 10 | sylancr 695 |
. . . . 5
|
12 | 4, 11 | eqtrd 2656 |
. . . 4
f |
13 | 12 | opeq2d 4409 |
. . 3
f |
14 | 3, 13 | eqtr4d 2659 |
. 2
f f |
15 | | eqid 2622 |
. . . 4
cat
cat
|
16 | | eqid 2622 |
. . . 4
|
17 | | eqid 2622 |
. . . 4
cat
cat
|
18 | | eqid 2622 |
. . . 4
|
19 | | eqid 2622 |
. . . 4
cat cat |
20 | | eqid 2622 |
. . . 4
|
21 | | eqid 2622 |
. . . 4
comp
cat comp cat |
22 | | eqid 2622 |
. . . 4
comp comp |
23 | | eqid 2622 |
. . . . 5
cat cat |
24 | 23, 2 | subccat 16508 |
. . . 4
cat
|
25 | | funcrcl 16523 |
. . . . . 6
|
26 | 1, 25 | syl 17 |
. . . . 5
|
27 | 26 | simprd 479 |
. . . 4
|
28 | | eqid 2622 |
. . . . . . 7
|
29 | | relfunc 16522 |
. . . . . . . 8
|
30 | | 1st2ndbr 7217 |
. . . . . . . 8
|
31 | 29, 1, 30 | sylancr 695 |
. . . . . . 7
|
32 | 28, 16, 31 | funcf1 16526 |
. . . . . 6
|
33 | | eqidd 2623 |
. . . . . . . 8
|
34 | 2, 33 | subcfn 16501 |
. . . . . . 7
|
35 | 2, 34, 28 | subcss1 16502 |
. . . . . 6
|
36 | 32, 35 | fssresd 6071 |
. . . . 5
|
37 | 26 | simpld 475 |
. . . . . . 7
|
38 | 23, 28, 37, 34, 35 | rescbas 16489 |
. . . . . 6
cat |
39 | 38 | feq2d 6031 |
. . . . 5
cat
|
40 | 36, 39 | mpbid 222 |
. . . 4
cat
|
41 | | fvex 6201 |
. . . . . . 7
|
42 | 41 | resex 5443 |
. . . . . 6
|
43 | | eqid 2622 |
. . . . . 6
|
44 | 42, 43 | fnmpti 6022 |
. . . . 5
|
45 | 12 | eqcomd 2628 |
. . . . . 6
f |
46 | | fndm 5990 |
. . . . . . . 8
|
47 | 34, 46 | syl 17 |
. . . . . . 7
|
48 | 38 | sqxpeqd 5141 |
. . . . . . 7
cat
cat
|
49 | 47, 48 | eqtrd 2656 |
. . . . . 6
cat cat |
50 | 45, 49 | fneq12d 5983 |
. . . . 5
f cat cat |
51 | 44, 50 | mpbii 223 |
. . . 4
f cat cat |
52 | | eqid 2622 |
. . . . . . . 8
|
53 | 31 | adantr 481 |
. . . . . . . 8
cat
cat
|
54 | 35 | adantr 481 |
. . . . . . . . 9
cat
cat
|
55 | | simprl 794 |
. . . . . . . . . 10
cat
cat
cat
|
56 | 38 | adantr 481 |
. . . . . . . . . 10
cat
cat
cat |
57 | 55, 56 | eleqtrrd 2704 |
. . . . . . . . 9
cat
cat
|
58 | 54, 57 | sseldd 3604 |
. . . . . . . 8
cat
cat
|
59 | | simprr 796 |
. . . . . . . . . 10
cat
cat
cat
|
60 | 59, 56 | eleqtrrd 2704 |
. . . . . . . . 9
cat
cat
|
61 | 54, 60 | sseldd 3604 |
. . . . . . . 8
cat
cat
|
62 | 28, 52, 18, 53, 58, 61 | funcf2 16528 |
. . . . . . 7
cat
cat
|
63 | 2 | adantr 481 |
. . . . . . . 8
cat
cat
Subcat |
64 | 34 | adantr 481 |
. . . . . . . 8
cat
cat
|
65 | 63, 64, 52, 57, 60 | subcss2 16503 |
. . . . . . 7
cat
cat
|
66 | 62, 65 | fssresd 6071 |
. . . . . 6
cat
cat
|
67 | 1 | adantr 481 |
. . . . . . . 8
cat
cat
|
68 | 67, 63, 64, 57, 60 | resf2nd 16555 |
. . . . . . 7
cat
cat
f |
69 | 68 | feq1d 6030 |
. . . . . 6
cat
cat
f
|
70 | 66, 69 | mpbird 247 |
. . . . 5
cat
cat
f
|
71 | 23, 28, 37, 34, 35 | reschom 16490 |
. . . . . . . 8
cat
|
72 | 71 | adantr 481 |
. . . . . . 7
cat
cat
cat
|
73 | 72 | oveqd 6667 |
. . . . . 6
cat
cat
cat |
74 | | fvres 6207 |
. . . . . . . . 9
|
75 | 57, 74 | syl 17 |
. . . . . . . 8
cat
cat
|
76 | | fvres 6207 |
. . . . . . . . 9
|
77 | 60, 76 | syl 17 |
. . . . . . . 8
cat
cat
|
78 | 75, 77 | oveq12d 6668 |
. . . . . . 7
cat
cat
|
79 | 78 | eqcomd 2628 |
. . . . . 6
cat
cat
|
80 | 73, 79 | feq23d 6040 |
. . . . 5
cat
cat
f
f cat
|
81 | 70, 80 | mpbid 222 |
. . . 4
cat
cat
f cat
|
82 | 1 | adantr 481 |
. . . . . . 7
cat
|
83 | 2 | adantr 481 |
. . . . . . 7
cat
Subcat |
84 | 34 | adantr 481 |
. . . . . . 7
cat
|
85 | 38 | eleq2d 2687 |
. . . . . . . 8
cat |
86 | 85 | biimpar 502 |
. . . . . . 7
cat
|
87 | 82, 83, 84, 86, 86 | resf2nd 16555 |
. . . . . 6
cat f |
88 | | eqid 2622 |
. . . . . . . 8
|
89 | 23, 83, 84, 88, 86 | subcid 16507 |
. . . . . . 7
cat cat |
90 | 89 | eqcomd 2628 |
. . . . . 6
cat
cat |
91 | 87, 90 | fveq12d 6197 |
. . . . 5
cat f cat |
92 | 31 | adantr 481 |
. . . . . . 7
cat |
93 | 38, 35 | eqsstr3d 3640 |
. . . . . . . 8
cat |
94 | 93 | sselda 3603 |
. . . . . . 7
cat
|
95 | 28, 88, 20, 92, 94 | funcid 16530 |
. . . . . 6
cat |
96 | 83, 84, 86, 88 | subcidcl 16504 |
. . . . . . 7
cat |
97 | | fvres 6207 |
. . . . . . 7
|
98 | 96, 97 | syl 17 |
. . . . . 6
cat |
99 | 86, 74 | syl 17 |
. . . . . . 7
cat |
100 | 99 | fveq2d 6195 |
. . . . . 6
cat |
101 | 95, 98, 100 | 3eqtr4d 2666 |
. . . . 5
cat
|
102 | 91, 101 | eqtrd 2656 |
. . . 4
cat f cat |
103 | 2 | 3ad2ant1 1082 |
. . . . . . . 8
cat
cat
cat cat cat
Subcat |
104 | 34 | 3ad2ant1 1082 |
. . . . . . . 8
cat
cat
cat cat cat
|
105 | | simp21 1094 |
. . . . . . . . 9
cat
cat
cat cat cat
cat |
106 | 38 | 3ad2ant1 1082 |
. . . . . . . . 9
cat
cat
cat cat cat
cat |
107 | 105, 106 | eleqtrrd 2704 |
. . . . . . . 8
cat
cat
cat cat cat
|
108 | | eqid 2622 |
. . . . . . . 8
comp comp |
109 | | simp22 1095 |
. . . . . . . . 9
cat
cat
cat cat cat
cat |
110 | 109, 106 | eleqtrrd 2704 |
. . . . . . . 8
cat
cat
cat cat cat
|
111 | | simp23 1096 |
. . . . . . . . 9
cat
cat
cat cat cat
cat |
112 | 111, 106 | eleqtrrd 2704 |
. . . . . . . 8
cat
cat
cat cat cat
|
113 | | simp3l 1089 |
. . . . . . . . 9
cat
cat
cat cat cat
cat
|
114 | 71 | 3ad2ant1 1082 |
. . . . . . . . . 10
cat
cat
cat cat cat
cat |
115 | 114 | oveqd 6667 |
. . . . . . . . 9
cat
cat
cat cat cat
cat
|
116 | 113, 115 | eleqtrrd 2704 |
. . . . . . . 8
cat
cat
cat cat cat
|
117 | | simp3r 1090 |
. . . . . . . . 9
cat
cat
cat cat cat
cat
|
118 | 114 | oveqd 6667 |
. . . . . . . . 9
cat
cat
cat cat cat
cat
|
119 | 117, 118 | eleqtrrd 2704 |
. . . . . . . 8
cat
cat
cat cat cat
|
120 | 103, 104,
107, 108, 110, 112, 116, 119 | subccocl 16505 |
. . . . . . 7
cat
cat
cat cat cat
comp |
121 | | fvres 6207 |
. . . . . . 7
comp comp comp |
122 | 120, 121 | syl 17 |
. . . . . 6
cat
cat
cat cat cat
comp comp |
123 | 31 | 3ad2ant1 1082 |
. . . . . . 7
cat
cat
cat cat cat
|
124 | 35 | 3ad2ant1 1082 |
. . . . . . . 8
cat
cat
cat cat cat
|
125 | 124, 107 | sseldd 3604 |
. . . . . . 7
cat
cat
cat cat cat
|
126 | 124, 110 | sseldd 3604 |
. . . . . . 7
cat
cat
cat cat cat
|
127 | 124, 112 | sseldd 3604 |
. . . . . . 7
cat
cat
cat cat cat
|
128 | 103, 104,
52, 107, 110 | subcss2 16503 |
. . . . . . . 8
cat
cat
cat cat cat
|
129 | 128, 116 | sseldd 3604 |
. . . . . . 7
cat
cat
cat cat cat
|
130 | 103, 104,
52, 110, 112 | subcss2 16503 |
. . . . . . . 8
cat
cat
cat cat cat
|
131 | 130, 119 | sseldd 3604 |
. . . . . . 7
cat
cat
cat cat cat
|
132 | 28, 52, 108, 22, 123, 125, 126, 127, 129, 131 | funcco 16531 |
. . . . . 6
cat
cat
cat cat cat
comp comp |
133 | 122, 132 | eqtrd 2656 |
. . . . 5
cat
cat
cat cat cat
comp comp |
134 | 1 | 3ad2ant1 1082 |
. . . . . . 7
cat
cat
cat cat cat
|
135 | 134, 103,
104, 107, 112 | resf2nd 16555 |
. . . . . 6
cat
cat
cat cat cat
f |
136 | 23, 28, 37, 34, 35, 108 | rescco 16492 |
. . . . . . . . . 10
comp comp cat |
137 | 136 | 3ad2ant1 1082 |
. . . . . . . . 9
cat
cat
cat cat cat
comp comp
cat |
138 | 137 | eqcomd 2628 |
. . . . . . . 8
cat
cat
cat cat cat
comp cat comp |
139 | 138 | oveqd 6667 |
. . . . . . 7
cat
cat
cat cat cat
comp cat
comp |
140 | 139 | oveqd 6667 |
. . . . . 6
cat
cat
cat cat cat
comp cat comp |
141 | 135, 140 | fveq12d 6197 |
. . . . 5
cat
cat
cat cat cat
f comp cat comp |
142 | 107, 74 | syl 17 |
. . . . . . . 8
cat
cat
cat cat cat
|
143 | 110, 76 | syl 17 |
. . . . . . . 8
cat
cat
cat cat cat
|
144 | 142, 143 | opeq12d 4410 |
. . . . . . 7
cat
cat
cat cat cat
|
145 | | fvres 6207 |
. . . . . . . 8
|
146 | 112, 145 | syl 17 |
. . . . . . 7
cat
cat
cat cat cat
|
147 | 144, 146 | oveq12d 6668 |
. . . . . 6
cat
cat
cat cat cat
comp comp |
148 | 134, 103,
104, 110, 112 | resf2nd 16555 |
. . . . . . . 8
cat
cat
cat cat cat
f |
149 | 148 | fveq1d 6193 |
. . . . . . 7
cat
cat
cat cat cat
f |
150 | | fvres 6207 |
. . . . . . . 8
|
151 | 119, 150 | syl 17 |
. . . . . . 7
cat
cat
cat cat cat
|
152 | 149, 151 | eqtrd 2656 |
. . . . . 6
cat
cat
cat cat cat
f |
153 | 134, 103,
104, 107, 110 | resf2nd 16555 |
. . . . . . . 8
cat
cat
cat cat cat
f |
154 | 153 | fveq1d 6193 |
. . . . . . 7
cat
cat
cat cat cat
f |
155 | | fvres 6207 |
. . . . . . . 8
|
156 | 116, 155 | syl 17 |
. . . . . . 7
cat
cat
cat cat cat
|
157 | 154, 156 | eqtrd 2656 |
. . . . . 6
cat
cat
cat cat cat
f |
158 | 147, 152,
157 | oveq123d 6671 |
. . . . 5
cat
cat
cat cat cat
f
comp f comp |
159 | 133, 141,
158 | 3eqtr4d 2666 |
. . . 4
cat
cat
cat cat cat
f comp cat f
comp f |
160 | 15, 16, 17, 18, 19, 20, 21, 22, 24, 27, 40, 51, 81, 102, 159 | isfuncd 16525 |
. . 3
cat f |
161 | | df-br 4654 |
. . 3
cat f
f cat
|
162 | 160, 161 | sylib 208 |
. 2
f cat
|
163 | 14, 162 | eqeltrd 2701 |
1
f cat
|