Theorem ovmpt3rab1

Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
	ovmpt3rab1.m	|- ( ( x = X /\ y = Y ) -> M = K )
	ovmpt3rab1.n	|- ( ( x = X /\ y = Y ) -> N = L )
	ovmpt3rab1.p	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
	ovmpt3rab1.x	|- F/ x ps
	ovmpt3rab1.y	|- F/ y ps
Assertion	ovmpt3rab1	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | ps } ) )

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
2		ovmpt3rab1.m	|- ( ( x = X /\ y = Y ) -> M = K )
3		ovmpt3rab1.n	|- ( ( x = X /\ y = Y ) -> N = L )
4		ovmpt3rab1.p	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
5		ovmpt3rab1.x	|- F/ x ps
6		ovmpt3rab1.y	|- F/ y ps
7	1	a1i	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) ) )
8	3 4	rabeqbidv	|- ( ( x = X /\ y = Y ) -> { a e. N | ph } = { a e. L | ps } )
9	2 8	mpteq12dv	|- ( ( x = X /\ y = Y ) -> ( z e. M |-> { a e. N | ph } ) = ( z e. K |-> { a e. L | ps } ) )
10	9	adantl	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ ( x = X /\ y = Y ) ) -> ( z e. M |-> { a e. N | ph } ) = ( z e. K |-> { a e. L | ps } ) )
11		eqidd	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ x = X ) -> _V = _V )
12		elex	|- ( X e. V -> X e. _V )
13	12	3ad2ant1	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> X e. _V )
14		elex	|- ( Y e. W -> Y e. _V )
15	14	3ad2ant2	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> Y e. _V )
16		mptexg	|- ( K e. U -> ( z e. K |-> { a e. L | ps } ) e. _V )
17	16	3ad2ant3	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> ( z e. K |-> { a e. L | ps } ) e. _V )
18		nfv	|- F/ x ( X e. V /\ Y e. W /\ K e. U )
19		nfv	|- F/ y ( X e. V /\ Y e. W /\ K e. U )
20		nfcv	|- F/_ y X
21		nfcv	|- F/_ x Y
22		nfcv	|- F/_ x K
23		nfcv	|- F/_ x L
24	5 23	nfrabw	|- F/_ x { a e. L | ps }
25	22 24	nfmpt	|- F/_ x ( z e. K |-> { a e. L | ps } )
26		nfcv	|- F/_ y K
27		nfcv	|- F/_ y L
28	6 27	nfrabw	|- F/_ y { a e. L | ps }
29	26 28	nfmpt	|- F/_ y ( z e. K |-> { a e. L | ps } )
30	7 10 11 13 15 17 18 19 20 21 25 29	ovmpodxf	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | ps } ) )