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

Metamath Proof Explorer

Theorem ot2ndg

Description: Extract the second member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 2-May-2015)

Ref Expression
Assertion ot2ndg 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )

Proof

Step Hyp Ref Expression
1 df-ot 
 |-  <. A , B , C >. = <. <. A , B >. , C >.
2 1 fveq2i 
 |-  ( 1st ` <. A , B , C >. ) = ( 1st ` <. <. A , B >. , C >. )
3 opex 
 |-  <. A , B >. e. _V
4 op1stg 
 |-  ( ( <. A , B >. e. _V /\ C e. X ) -> ( 1st ` <. <. A , B >. , C >. ) = <. A , B >. )
5 3 4 mpan 
 |-  ( C e. X -> ( 1st ` <. <. A , B >. , C >. ) = <. A , B >. )
6 2 5 eqtrid 
 |-  ( C e. X -> ( 1st ` <. A , B , C >. ) = <. A , B >. )
7 6 fveq2d 
 |-  ( C e. X -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = ( 2nd ` <. A , B >. ) )
8 op2ndg 
 |-  ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
9 7 8 sylan9eqr 
 |-  ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )
10 9 3impa 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )