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↾BFndom⁡A↾B
4 dffn5 ⊢A↾BFndom⁡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⟼xA↾B⁡x
8 5 7 eqtrdi ⊢Fun⁡A∧B∈C→A↾B=ran⁡x∈dom⁡A↾B⟼xA↾B⁡x
9 opex ⊢xA↾B⁡x∈V
10 eqid ⊢x∈dom⁡A↾B⟼xA↾B⁡x=x∈dom⁡A↾B⟼xA↾B⁡x
11 9 10 dmmpti ⊢dom⁡x∈dom⁡A↾B⟼xA↾B⁡x=dom⁡A↾B
12 11 imaeq2i ⊢x∈dom⁡A↾B⟼xA↾B⁡xdom⁡x∈dom⁡A↾B⟼xA↾B⁡x=x∈dom⁡A↾B⟼xA↾B⁡xdom⁡A↾B
13 imadmrn ⊢x∈dom⁡A↾B⟼xA↾B⁡xdom⁡x∈dom⁡A↾B⟼xA↾B⁡x=ran⁡x∈dom⁡A↾B⟼xA↾B⁡x
14 12 13 eqtr3i ⊢x∈dom⁡A↾B⟼xA↾B⁡xdom⁡A↾B=ran⁡x∈dom⁡A↾B⟼xA↾B⁡x
15 8 14 eqtr4di ⊢Fun⁡A∧B∈C→A↾B=x∈dom⁡A↾B⟼xA↾B⁡xdom⁡A↾B
16 funmpt ⊢Fun⁡x∈dom⁡A↾B⟼xA↾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⟼xA↾B⁡x∧dom⁡A↾B∈V→x∈dom⁡A↾B⟼xA↾B⁡xdom⁡A↾B∈V
20 16 18 19 sylancr ⊢Fun⁡A∧B∈C→x∈dom⁡A↾B⟼xA↾B⁡xdom⁡A↾B∈V
21 15 20 eqeltrd ⊢Fun⁡A∧B∈C→A↾B∈V