Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

	Ref	Expression
Hypotheses	elovmporab.o	|- O = ( x e. _V , y e. _V |-> { z e. M | ph } )
	elovmporab.v	|- ( ( X e. _V /\ Y e. _V ) -> M e. _V )
Assertion	elovmporab	|- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) )

Proof

Step	Hyp	Ref	Expression
1		elovmporab.o	|- O = ( x e. _V , y e. _V |-> { z e. M | ph } )
2		elovmporab.v	|- ( ( X e. _V /\ Y e. _V ) -> M e. _V )
3	1	elmpocl	|- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V ) )
4	1	a1i	|- ( ( X e. _V /\ Y e. _V ) -> O = ( x e. _V , y e. _V |-> { z e. M | ph } ) )
5		sbceq1a	|- ( y = Y -> ( ph <-> [. Y / y ]. ph ) )
6		sbceq1a	|- ( x = X -> ( [. Y / y ]. ph <-> [. X / x ]. [. Y / y ]. ph ) )
7	5 6	sylan9bbr	|- ( ( x = X /\ y = Y ) -> ( ph <-> [. X / x ]. [. Y / y ]. ph ) )
8	7	adantl	|- ( ( ( X e. _V /\ Y e. _V ) /\ ( x = X /\ y = Y ) ) -> ( ph <-> [. X / x ]. [. Y / y ]. ph ) )
9	8	rabbidv	|- ( ( ( X e. _V /\ Y e. _V ) /\ ( x = X /\ y = Y ) ) -> { z e. M | ph } = { z e. M | [. X / x ]. [. Y / y ]. ph } )
10		eqidd	|- ( ( ( X e. _V /\ Y e. _V ) /\ x = X ) -> _V = _V )
11		simpl	|- ( ( X e. _V /\ Y e. _V ) -> X e. _V )
12		simpr	|- ( ( X e. _V /\ Y e. _V ) -> Y e. _V )
13		rabexg	|- ( M e. _V -> { z e. M | [. X / x ]. [. Y / y ]. ph } e. _V )
14	2 13	syl	|- ( ( X e. _V /\ Y e. _V ) -> { z e. M | [. X / x ]. [. Y / y ]. ph } e. _V )
15		nfcv	|- F/_ x X
16	15	nfel1	|- F/ x X e. _V
17		nfcv	|- F/_ x Y
18	17	nfel1	|- F/ x Y e. _V
19	16 18	nfan	|- F/ x ( X e. _V /\ Y e. _V )
20		nfcv	|- F/_ y X
21	20	nfel1	|- F/ y X e. _V
22		nfcv	|- F/_ y Y
23	22	nfel1	|- F/ y Y e. _V
24	21 23	nfan	|- F/ y ( X e. _V /\ Y e. _V )
25		nfsbc1v	|- F/ x [. X / x ]. [. Y / y ]. ph
26		nfcv	|- F/_ x M
27	25 26	nfrabw	|- F/_ x { z e. M | [. X / x ]. [. Y / y ]. ph }
28		nfsbc1v	|- F/ y [. Y / y ]. ph
29	20 28	nfsbcw	|- F/ y [. X / x ]. [. Y / y ]. ph
30		nfcv	|- F/_ y M
31	29 30	nfrabw	|- F/_ y { z e. M | [. X / x ]. [. Y / y ]. ph }
32	4 9 10 11 12 14 19 24 20 17 27 31	ovmpodxf	|- ( ( X e. _V /\ Y e. _V ) -> ( X O Y ) = { z e. M | [. X / x ]. [. Y / y ]. ph } )
33	32	eleq2d	|- ( ( X e. _V /\ Y e. _V ) -> ( Z e. ( X O Y ) <-> Z e. { z e. M | [. X / x ]. [. Y / y ]. ph } ) )
34		df-3an	|- ( ( X e. _V /\ Y e. _V /\ Z e. M ) <-> ( ( X e. _V /\ Y e. _V ) /\ Z e. M ) )
35	34	simplbi2com	|- ( Z e. M -> ( ( X e. _V /\ Y e. _V ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) ) )
36		elrabi	|- ( Z e. { z e. M | [. X / x ]. [. Y / y ]. ph } -> Z e. M )
37	35 36	syl11	|- ( ( X e. _V /\ Y e. _V ) -> ( Z e. { z e. M | [. X / x ]. [. Y / y ]. ph } -> ( X e. _V /\ Y e. _V /\ Z e. M ) ) )
38	33 37	sylbid	|- ( ( X e. _V /\ Y e. _V ) -> ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) ) )
39	3 38	mpcom	|- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) )