Metamath Proof Explorer

Theorem mpoxopoveq

Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017)

Ref Expression
Hypothesis mpoxopoveq.f 
|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )
Assertion mpoxopoveq 
|- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )

Proof

Step Hyp Ref Expression
1 mpoxopoveq.f 
 |-  F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )
2 1 a1i 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } ) )
3 fveq2 
 |-  ( x = <. V , W >. -> ( 1st ` x ) = ( 1st ` <. V , W >. ) )
4 op1stg 
 |-  ( ( V e. X /\ W e. Y ) -> ( 1st ` <. V , W >. ) = V )
5 4 adantr 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( 1st ` <. V , W >. ) = V )
6 3 5 sylan9eqr 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ x = <. V , W >. ) -> ( 1st ` x ) = V )
7 6 adantrr 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( 1st ` x ) = V )
8 sbceq1a 
 |-  ( y = K -> ( ph <-> [. K / y ]. ph ) )
9 8 adantl 
 |-  ( ( x = <. V , W >. /\ y = K ) -> ( ph <-> [. K / y ]. ph ) )
10 9 adantl 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( ph <-> [. K / y ]. ph ) )
11 sbceq1a 
 |-  ( x = <. V , W >. -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
12 11 adantr 
 |-  ( ( x = <. V , W >. /\ y = K ) -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
13 12 adantl 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( [. K / y ]. ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
14 10 13 bitrd 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> ( ph <-> [. <. V , W >. / x ]. [. K / y ]. ph ) )
15 7 14 rabeqbidv 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ K e. V ) /\ ( x = <. V , W >. /\ y = K ) ) -> { n e. ( 1st ` x ) | ph } = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
16 opex 
 |-  <. V , W >. e. _V
17 16 a1i 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> <. V , W >. e. _V )
18 simpr 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> K e. V )
19 rabexg 
 |-  ( V e. X -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } e. _V )
20 19 ad2antrr 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } e. _V )
21 equid 
 |-  z = z
22 nfvd 
 |-  ( z = z -> F/ x ( ( V e. X /\ W e. Y ) /\ K e. V ) )
23 21 22 ax-mp 
 |-  F/ x ( ( V e. X /\ W e. Y ) /\ K e. V )
24 nfvd 
 |-  ( z = z -> F/ y ( ( V e. X /\ W e. Y ) /\ K e. V ) )
25 21 24 ax-mp 
 |-  F/ y ( ( V e. X /\ W e. Y ) /\ K e. V )
26 nfcv 
 |-  F/_ y <. V , W >.
27 nfcv 
 |-  F/_ x K
28 nfsbc1v 
 |-  F/ x [. <. V , W >. / x ]. [. K / y ]. ph
29 nfcv 
 |-  F/_ x V
30 28 29 nfrabw 
 |-  F/_ x { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph }
31 nfsbc1v 
 |-  F/ y [. K / y ]. ph
32 26 31 nfsbcw 
 |-  F/ y [. <. V , W >. / x ]. [. K / y ]. ph
33 nfcv 
 |-  F/_ y V
34 32 33 nfrabw 
 |-  F/_ y { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph }
35 2 15 6 17 18 20 23 25 26 27 30 34 ovmpodxf 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )