Metamath Proof Explorer

Theorem ot1stg

Description: Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg , ot2ndg , ot3rdg .) (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 2-May-2015)

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

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 -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = ( 1st ` <. A , B >. ) )
8 op1stg 
 |-  ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )
9 7 8 sylan9eqr 
 |-  ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A )
10 9 3impa 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A )