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