Metamath Proof Explorer

Theorem 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 ⊢A∈V
mpoexw.2 ⊢B∈V
mpoexw.3 ⊢D∈V
mpoexw.4 ⊢∀x∈A∀y∈BC∈D
Assertion mpoexw ⊢x∈A,y∈B⟼C∈V

Proof

Step Hyp Ref Expression
1 mpoexw.1 ⊢A∈V
2 mpoexw.2 ⊢B∈V
3 mpoexw.3 ⊢D∈V
4 mpoexw.4 ⊢∀x∈A∀y∈BC∈D
5 eqid ⊢x∈A,y∈B⟼C=x∈A,y∈B⟼C
6 5 mpofun ⊢Fun⁡x∈A,y∈B⟼C
7 5 dmmpoga ⊢∀x∈A∀y∈BC∈D→dom⁡x∈A,y∈B⟼C=A×B
8 4 7 ax-mp ⊢dom⁡x∈A,y∈B⟼C=A×B
9 1 2 xpex ⊢A×B∈V
10 8 9 eqeltri ⊢dom⁡x∈A,y∈B⟼C∈V
11 5 rnmpo ⊢ran⁡x∈A,y∈B⟼C=z|∃x∈A∃y∈Bz=C
12 4 rspec ⊢x∈A→∀y∈BC∈D
13 12 r19.21bi ⊢x∈A∧y∈B→C∈D
14 eleq1a ⊢C∈D→z=C→z∈D
15 13 14 syl ⊢x∈A∧y∈B→z=C→z∈D
16 15 rexlimdva ⊢x∈A→∃y∈Bz=C→z∈D
17 16 rexlimiv ⊢∃x∈A∃y∈Bz=C→z∈D
18 17 abssi ⊢z|∃x∈A∃y∈Bz=C⊆D
19 3 18 ssexi ⊢z|∃x∈A∃y∈Bz=C∈V
20 11 19 eqeltri ⊢ran⁡x∈A,y∈B⟼C∈V
21 funexw ⊢Fun⁡x∈A,y∈B⟼C∧dom⁡x∈A,y∈B⟼C∈V∧ran⁡x∈A,y∈B⟼C∈V→x∈A,y∈B⟼C∈V
22 6 10 20 21 mp3an ⊢x∈A,y∈B⟼C∈V