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 ⊢ A ∈ V
mptexw.2 ⊢ C ∈ V
mptexw.3 ⊢ ∀ x ∈ A B ∈ C
Assertion mptexw ⊢ x ∈ A ⟼ B ∈ V

Proof

Step Hyp Ref Expression
1 mptexw.1 ⊢ A ∈ V
2 mptexw.2 ⊢ C ∈ V
3 mptexw.3 ⊢ ∀ x ∈ A B ∈ C
4 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
5 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
6 5 dmmptss ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
7 1 6 ssexi ⊢ dom ⁡ x ∈ A ⟼ B ∈ V
8 5 rnmptss ⊢ ∀ x ∈ A B ∈ C → ran ⁡ x ∈ A ⟼ B ⊆ C
9 3 8 ax-mp ⊢ ran ⁡ x ∈ A ⟼ B ⊆ C
10 2 9 ssexi ⊢ ran ⁡ x ∈ A ⟼ B ∈ V
11 funexw ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ V ∧ ran ⁡ x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
12 4 7 10 11 mp3an ⊢ x ∈ A ⟼ B ∈ V