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