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