Description: Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fssrescdmd.f | |
|
fssrescdmd.c | |
||
fssrescdmd.d | |
||
Assertion | fssrescdmd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fssrescdmd.f | |
|
2 | fssrescdmd.c | |
|
3 | fssrescdmd.d | |
|
4 | 1 | ffnd | |
5 | 4 2 | fnssresd | |
6 | resima | |
|
7 | 6 3 | eqsstrid | |
8 | 1 | ffund | |
9 | 8 | funresd | |
10 | 1 | fdmd | |
11 | 2 10 | sseqtrrd | |
12 | ssdmres | |
|
13 | 12 | a1i | |
14 | eqcom | |
|
15 | 13 14 | bitrdi | |
16 | 11 15 | mpbid | |
17 | 16 | eqimssd | |
18 | funimass4 | |
|
19 | 9 17 18 | syl2anc | |
20 | 7 19 | mpbid | |
21 | ffnfv | |
|
22 | 5 20 21 | sylanbrc | |