Metamath Proof Explorer

Theorem elovmporab1w

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. Version of elovmporab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 elovmporab1w.o 
 |-  O = ( x e. _V , y e. _V |-> { z e. [_ x / m ]_ M | ph } )
2 elovmporab1w.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 nfcsbw 
 |-  F/_ x [_ X / m ]_ M
30 27 29 nfrabw 
 |-  F/_ x { z e. [_ X / m ]_ M | [. X / x ]. [. Y / y ]. ph }
31 nfsbc1v 
 |-  F/ y [. Y / y ]. ph
32 22 31 nfsbcw 
 |-  F/ y [. X / x ]. [. Y / y ]. ph
33 nfcv 
 |-  F/_ y M
34 22 33 nfcsbw 
 |-  F/_ y [_ X / m ]_ M
35 32 34 nfrabw 
 |-  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 ) )