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