mpoexw

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

	Ref	Expression
Hypotheses	mpoexw.1	⊢ 𝐴 ∈ V
	mpoexw.2	⊢ 𝐵 ∈ V
	mpoexw.3	⊢ 𝐷 ∈ V
	mpoexw.4	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷
Assertion	mpoexw	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		mpoexw.1	⊢ 𝐴 ∈ V
2		mpoexw.2	⊢ 𝐵 ∈ V
3		mpoexw.3	⊢ 𝐷 ∈ V
4		mpoexw.4	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷
5		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
6	5	mpofun	⊢ Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
7	5	dmmpoga	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝐴 × 𝐵 ) )
8	4 7	ax-mp	⊢ dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝐴 × 𝐵 )
9	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
10	8 9	eqeltri	⊢ dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V
11	5	rnmpo	⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
12	4	rspec	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 )
13	12	r19.21bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
14		eleq1a	⊢ ( 𝐶 ∈ 𝐷 → ( 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
15	13 14	syl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
16	15	rexlimdva	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
17	16	rexlimiv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 )
18	17	abssi	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ⊆ 𝐷
19	3 18	ssexi	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ∈ V
20	11 19	eqeltri	⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V
21		funexw	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∧ dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ∧ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
22	6 10 20 21	mp3an	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V

Metamath Proof Explorer

Theorem mpoexw

Proof