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 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 funres ⊢ ( Fun 𝐴 → Fun ( 𝐴 ↾ 𝐵 ) )
2 1 adantr ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → Fun ( 𝐴 ↾ 𝐵 ) )
3 2 funfnd ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) )
4 dffn5 ⊢ ( ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) ↔ ( 𝐴 ↾ 𝐵 ) = ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ) )
5 3 4 sylib ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) = ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ) )
6 fvex ⊢ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ V
7 6 fnasrn ⊢ ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ) = ran ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ )
8 5 7 eqtrdi ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) = ran ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) )
9 opex ⊢ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ∈ V
10 eqid ⊢ ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ )
11 9 10 dmmpti ⊢ dom ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) = dom ( 𝐴 ↾ 𝐵 )
12 11 imaeq2i ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) ) = ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝐴 ↾ 𝐵 ) )
13 imadmrn ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) ) = ran ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ )
14 12 13 eqtr3i ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝐴 ↾ 𝐵 ) ) = ran ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ )
15 8 14 eqtr4di ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) = ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝐴 ↾ 𝐵 ) ) )
16 funmpt ⊢ Fun ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ )
17 dmresexg ⊢ ( 𝐵 ∈ 𝐶 → dom ( 𝐴 ↾ 𝐵 ) ∈ V )
18 17 adantl ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → dom ( 𝐴 ↾ 𝐵 ) ∈ V )
19 funimaexg ⊢ ( ( Fun ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) ∧ dom ( 𝐴 ↾ 𝐵 ) ∈ V ) → ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝐴 ↾ 𝐵 ) ) ∈ V )
20 16 18 19 sylancr ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ↦ ⟨ 𝑥 , ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ⟩ ) “ dom ( 𝐴 ↾ 𝐵 ) ) ∈ V )
21 15 20 eqeltrd ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) ∈ V )