Metamath Proof Explorer


Theorem ffvresb

Description: A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion ffvresb FunFFA:ABxAxdomFFxB

Proof

Step Hyp Ref Expression
1 fdm FA:ABdomFA=A
2 dmres domFA=AdomF
3 inss2 AdomFdomF
4 2 3 eqsstri domFAdomF
5 1 4 eqsstrrdi FA:ABAdomF
6 5 sselda FA:ABxAxdomF
7 fvres xAFAx=Fx
8 7 adantl FA:ABxAFAx=Fx
9 ffvelrn FA:ABxAFAxB
10 8 9 eqeltrrd FA:ABxAFxB
11 6 10 jca FA:ABxAxdomFFxB
12 11 ralrimiva FA:ABxAxdomFFxB
13 simpl xdomFFxBxdomF
14 13 ralimi xAxdomFFxBxAxdomF
15 dfss3 AdomFxAxdomF
16 14 15 sylibr xAxdomFFxBAdomF
17 funfn FunFFFndomF
18 fnssres FFndomFAdomFFAFnA
19 17 18 sylanb FunFAdomFFAFnA
20 16 19 sylan2 FunFxAxdomFFxBFAFnA
21 simpr xdomFFxBFxB
22 7 eleq1d xAFAxBFxB
23 21 22 syl5ibr xAxdomFFxBFAxB
24 23 ralimia xAxdomFFxBxAFAxB
25 24 adantl FunFxAxdomFFxBxAFAxB
26 fnfvrnss FAFnAxAFAxBranFAB
27 20 25 26 syl2anc FunFxAxdomFFxBranFAB
28 df-f FA:ABFAFnAranFAB
29 20 27 28 sylanbrc FunFxAxdomFFxBFA:AB
30 29 ex FunFxAxdomFFxBFA:AB
31 12 30 impbid2 FunFFA:ABxAxdomFFxB