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 )