Theorem mpoexxg2

Description: Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg . (Contributed by AV, 30-Mar-2019)

	Ref	Expression
Hypothesis	mpoexxg2.1	|- F = ( x e. A , y e. B |-> C )
Assertion	mpoexxg2	|- ( ( B e. R /\ A. y e. B A e. S ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		mpoexxg2.1	|- F = ( x e. A , y e. B |-> C )
2	1	mpofun	|- Fun F
3	1	dmmpossx2	|- dom F C_ U_ y e. B ( A X. { y } )
4		vsnex	|- { y } e. _V
5		xpexg	|- ( ( A e. S /\ { y } e. _V ) -> ( A X. { y } ) e. _V )
6	4 5	mpan2	|- ( A e. S -> ( A X. { y } ) e. _V )
7	6	ralimi	|- ( A. y e. B A e. S -> A. y e. B ( A X. { y } ) e. _V )
8		iunexg	|- ( ( B e. R /\ A. y e. B ( A X. { y } ) e. _V ) -> U_ y e. B ( A X. { y } ) e. _V )
9	7 8	sylan2	|- ( ( B e. R /\ A. y e. B A e. S ) -> U_ y e. B ( A X. { y } ) e. _V )
10		ssexg	|- ( ( dom F C_ U_ y e. B ( A X. { y } ) /\ U_ y e. B ( A X. { y } ) e. _V ) -> dom F e. _V )
11	3 9 10	sylancr	|- ( ( B e. R /\ A. y e. B A e. S ) -> dom F e. _V )
12		funex	|- ( ( Fun F /\ dom F e. _V ) -> F e. _V )
13	2 11 12	sylancr	|- ( ( B e. R /\ A. y e. B A e. S ) -> F e. _V )