Metamath Proof Explorer


Theorem resfunexg

Description: The restriction of a function to a set exists. Compare Proposition 6.17 of TakeutiZaring p. 28. (Contributed by NM, 7-Apr-1995) (Revised by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion resfunexg Fun A B C A B V

Proof

Step Hyp Ref Expression
1 funres Fun A Fun A B
2 1 adantr Fun A B C Fun A B
3 2 funfnd Fun A B C A B Fn dom A B
4 dffn5 A B Fn dom A B A B = x dom A B A B x
5 3 4 sylib Fun A B C A B = x dom A B A B x
6 fvex A B x V
7 6 fnasrn x dom A B A B x = ran x dom A B x A B x
8 5 7 syl6eq Fun A B C A B = ran x dom A B x A B x
9 opex x A B x V
10 eqid x dom A B x A B x = x dom A B x A B x
11 9 10 dmmpti dom x dom A B x A B x = dom A B
12 11 imaeq2i x dom A B x A B x dom x dom A B x A B x = x dom A B x A B x dom A B
13 imadmrn x dom A B x A B x dom x dom A B x A B x = ran x dom A B x A B x
14 12 13 eqtr3i x dom A B x A B x dom A B = ran x dom A B x A B x
15 8 14 syl6eqr Fun A B C A B = x dom A B x A B x dom A B
16 funmpt Fun x dom A B x A B x
17 dmresexg B C dom A B V
18 17 adantl Fun A B C dom A B V
19 funimaexg Fun x dom A B x A B x dom A B V x dom A B x A B x dom A B V
20 16 18 19 sylancr Fun A B C x dom A B x A B x dom A B V
21 15 20 eqeltrd Fun A B C A B V