This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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