Description: A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | ffvresb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdm | |
|
2 | dmres | |
|
3 | inss2 | |
|
4 | 2 3 | eqsstri | |
5 | 1 4 | eqsstrrdi | |
6 | 5 | sselda | |
7 | fvres | |
|
8 | 7 | adantl | |
9 | ffvelrn | |
|
10 | 8 9 | eqeltrrd | |
11 | 6 10 | jca | |
12 | 11 | ralrimiva | |
13 | simpl | |
|
14 | 13 | ralimi | |
15 | dfss3 | |
|
16 | 14 15 | sylibr | |
17 | funfn | |
|
18 | fnssres | |
|
19 | 17 18 | sylanb | |
20 | 16 19 | sylan2 | |
21 | simpr | |
|
22 | 7 | eleq1d | |
23 | 21 22 | syl5ibr | |
24 | 23 | ralimia | |
25 | 24 | adantl | |
26 | fnfvrnss | |
|
27 | 20 25 26 | syl2anc | |
28 | df-f | |
|
29 | 20 27 28 | sylanbrc | |
30 | 29 | ex | |
31 | 12 30 | impbid2 | |