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 eqtrdi ⊢ 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 eqtr4di ⊢ 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