Metamath Proof Explorer


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 } ) )