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

Metamath Proof Explorer

Theorem mpoxopn0yelv

Description: If there is an element of the 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, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017)

Ref Expression
Hypothesis mpoxopn0yelv.f 
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )
Assertion mpoxopn0yelv 
|- ( ( V e. X /\ W e. Y ) -> ( N e. ( <. V , W >. F K ) -> K e. V ) )

Proof

Step Hyp Ref Expression
1 mpoxopn0yelv.f 
 |-  F = ( x e. _V , y e. ( 1st ` x ) |-> C )
2 1 dmmpossx 
 |-  dom F C_ U_ x e. _V ( { x } X. ( 1st ` x ) )
3 elfvdm 
 |-  ( N e. ( F ` <. <. V , W >. , K >. ) -> <. <. V , W >. , K >. e. dom F )
4 df-ov 
 |-  ( <. V , W >. F K ) = ( F ` <. <. V , W >. , K >. )
5 3 4 eleq2s 
 |-  ( N e. ( <. V , W >. F K ) -> <. <. V , W >. , K >. e. dom F )
6 2 5 sselid 
 |-  ( N e. ( <. V , W >. F K ) -> <. <. V , W >. , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) )
7 fveq2 
 |-  ( x = <. V , W >. -> ( 1st ` x ) = ( 1st ` <. V , W >. ) )
8 7 opeliunxp2 
 |-  ( <. <. V , W >. , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) <-> ( <. V , W >. e. _V /\ K e. ( 1st ` <. V , W >. ) ) )
9 8 simprbi 
 |-  ( <. <. V , W >. , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) -> K e. ( 1st ` <. V , W >. ) )
10 6 9 syl 
 |-  ( N e. ( <. V , W >. F K ) -> K e. ( 1st ` <. V , W >. ) )
11 op1stg 
 |-  ( ( V e. X /\ W e. Y ) -> ( 1st ` <. V , W >. ) = V )
12 11 eleq2d 
 |-  ( ( V e. X /\ W e. Y ) -> ( K e. ( 1st ` <. V , W >. ) <-> K e. V ) )
13 10 12 imbitrid 
 |-  ( ( V e. X /\ W e. Y ) -> ( N e. ( <. V , W >. F K ) -> K e. V ) )