Metamath Proof Explorer


Theorem mptexw

Description: Weak version of mptex that holds without ax-rep . If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mptexw.1 𝐴 ∈ V
mptexw.2 𝐶 ∈ V
mptexw.3 𝑥𝐴 𝐵𝐶
Assertion mptexw ( 𝑥𝐴𝐵 ) ∈ V

Proof

Step Hyp Ref Expression
1 mptexw.1 𝐴 ∈ V
2 mptexw.2 𝐶 ∈ V
3 mptexw.3 𝑥𝐴 𝐵𝐶
4 funmpt Fun ( 𝑥𝐴𝐵 )
5 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
6 5 dmmptss dom ( 𝑥𝐴𝐵 ) ⊆ 𝐴
7 1 6 ssexi dom ( 𝑥𝐴𝐵 ) ∈ V
8 5 rnmptss ( ∀ 𝑥𝐴 𝐵𝐶 → ran ( 𝑥𝐴𝐵 ) ⊆ 𝐶 )
9 3 8 ax-mp ran ( 𝑥𝐴𝐵 ) ⊆ 𝐶
10 2 9 ssexi ran ( 𝑥𝐴𝐵 ) ∈ V
11 funexw ( ( Fun ( 𝑥𝐴𝐵 ) ∧ dom ( 𝑥𝐴𝐵 ) ∈ V ∧ ran ( 𝑥𝐴𝐵 ) ∈ V ) → ( 𝑥𝐴𝐵 ) ∈ V )
12 4 7 10 11 mp3an ( 𝑥𝐴𝐵 ) ∈ V