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

Metamath Proof Explorer

Theorem mpoxopoveqd

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, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017)

Ref Expression
Hypotheses mpoxopoveq.f 
|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )
mpoxopoveqd.1 
|- ( ps -> ( V e. X /\ W e. Y ) )
mpoxopoveqd.2 
|- ( ( ps /\ -. K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } = (/) )
Assertion mpoxopoveqd 
|- ( ps -> ( <. 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 mpoxopoveqd.1 
 |-  ( ps -> ( V e. X /\ W e. Y ) )
3 mpoxopoveqd.2 
 |-  ( ( ps /\ -. K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } = (/) )
4 1 mpoxopoveq 
 |-  ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
5 4 ex 
 |-  ( ( V e. X /\ W e. Y ) -> ( K e. V -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
6 5 2 syl11 
 |-  ( K e. V -> ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
7 df-nel 
 |-  ( K e/ V <-> -. K e. V )
8 1 mpoxopynvov0 
 |-  ( K e/ V -> ( <. V , W >. F K ) = (/) )
9 7 8 sylbir 
 |-  ( -. K e. V -> ( <. V , W >. F K ) = (/) )
10 9 adantr 
 |-  ( ( -. K e. V /\ ps ) -> ( <. V , W >. F K ) = (/) )
11 3 eqcomd 
 |-  ( ( ps /\ -. K e. V ) -> (/) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
12 11 ancoms 
 |-  ( ( -. K e. V /\ ps ) -> (/) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
13 10 12 eqtrd 
 |-  ( ( -. K e. V /\ ps ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
14 13 ex 
 |-  ( -. K e. V -> ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } ) )
15 6 14 pm2.61i 
 |-  ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )