This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. _V
mpoexw.2 
|- B e. _V
mpoexw.3 
|- D e. _V
mpoexw.4 
|- A. x e. A A. y e. B C e. D
Assertion mpoexw 
|- ( x e. A , y e. B |-> C ) e. _V

Proof

Step Hyp Ref Expression
1 mpoexw.1 
 |-  A e. _V
2 mpoexw.2 
 |-  B e. _V
3 mpoexw.3 
 |-  D e. _V
4 mpoexw.4 
 |-  A. x e. A A. y e. B C e. D
5 eqid 
 |-  ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
6 5 mpofun 
 |-  Fun ( x e. A , y e. B |-> C )
7 5 dmmpoga 
 |-  ( A. x e. A A. y e. B C e. D -> dom ( x e. A , y e. B |-> C ) = ( A X. B ) )
8 4 7 ax-mp 
 |-  dom ( x e. A , y e. B |-> C ) = ( A X. B )
9 1 2 xpex 
 |-  ( A X. B ) e. _V
10 8 9 eqeltri 
 |-  dom ( x e. A , y e. B |-> C ) e. _V
11 5 rnmpo 
 |-  ran ( x e. A , y e. B |-> C ) = { z | E. x e. A E. y e. B z = C }
12 4 rspec 
 |-  ( x e. A -> A. y e. B C e. D )
13 12 r19.21bi 
 |-  ( ( x e. A /\ y e. B ) -> C e. D )
14 eleq1a 
 |-  ( C e. D -> ( z = C -> z e. D ) )
15 13 14 syl 
 |-  ( ( x e. A /\ y e. B ) -> ( z = C -> z e. D ) )
16 15 rexlimdva 
 |-  ( x e. A -> ( E. y e. B z = C -> z e. D ) )
17 16 rexlimiv 
 |-  ( E. x e. A E. y e. B z = C -> z e. D )
18 17 abssi 
 |-  { z | E. x e. A E. y e. B z = C } C_ D
19 3 18 ssexi 
 |-  { z | E. x e. A E. y e. B z = C } e. _V
20 11 19 eqeltri 
 |-  ran ( x e. A , y e. B |-> C ) e. _V
21 funexw 
 |-  ( ( Fun ( x e. A , y e. B |-> C ) /\ dom ( x e. A , y e. B |-> C ) e. _V /\ ran ( x e. A , y e. B |-> C ) e. _V ) -> ( x e. A , y e. B |-> C ) e. _V )
22 6 10 20 21 mp3an 
 |-  ( x e. A , y e. B |-> C ) e. _V