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