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	syl5eq	|- ( 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 )