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 ∈ B C ∈ 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 ∈ B C ∈ 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 ∈ B C ∈ 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 ∈ B z = C
12 4 rspec ⊢ x ∈ A → ∀ y ∈ B C ∈ 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 ∈ B z = C → z ∈ D
17 16 rexlimiv ⊢ ∃ x ∈ A ∃ y ∈ B z = C → z ∈ D
18 17 abssi ⊢ z | ∃ x ∈ A ∃ y ∈ B z = C ⊆ D
19 3 18 ssexi ⊢ z | ∃ x ∈ A ∃ y ∈ B z = 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