Metamath Proof Explorer


Theorem elovmporab1

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elovmporab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

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

Proof

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