Metamath Proof Explorer


Theorem mptexgf

Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011) (Revised by Mario Carneiro, 31-Aug-2015) (Revised by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypothesis mptexgf.a 𝑥 𝐴
Assertion mptexgf ( 𝐴𝑉 → ( 𝑥𝐴𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 mptexgf.a 𝑥 𝐴
2 funmpt Fun ( 𝑥𝐴𝐵 )
3 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
4 3 dmmpt dom ( 𝑥𝐴𝐵 ) = { 𝑥𝐴𝐵 ∈ V }
5 tru
6 5 2a1i ( 𝑥𝐴 → ( 𝐵 ∈ V → ⊤ ) )
7 6 ss2rabi { 𝑥𝐴𝐵 ∈ V } ⊆ { 𝑥𝐴 ∣ ⊤ }
8 1 rabtru { 𝑥𝐴 ∣ ⊤ } = 𝐴
9 7 8 sseqtri { 𝑥𝐴𝐵 ∈ V } ⊆ 𝐴
10 4 9 eqsstri dom ( 𝑥𝐴𝐵 ) ⊆ 𝐴
11 ssexg ( ( dom ( 𝑥𝐴𝐵 ) ⊆ 𝐴𝐴𝑉 ) → dom ( 𝑥𝐴𝐵 ) ∈ V )
12 10 11 mpan ( 𝐴𝑉 → dom ( 𝑥𝐴𝐵 ) ∈ V )
13 funex ( ( Fun ( 𝑥𝐴𝐵 ) ∧ dom ( 𝑥𝐴𝐵 ) ∈ V ) → ( 𝑥𝐴𝐵 ) ∈ V )
14 2 12 13 sylancr ( 𝐴𝑉 → ( 𝑥𝐴𝐵 ) ∈ V )