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

Metamath Proof Explorer

Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Hypotheses elovmporab.o 
|- O = ( x e. _V , y e. _V |-> { z e. M | ph } )
elovmporab.v 
|- ( ( X e. _V /\ Y e. _V ) -> M e. _V )
Assertion elovmporab 
|- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) )

Proof

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