This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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