Metamath Proof Explorer

Theorem oteqimp

Description: The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018)

Ref Expression
Assertion oteqimp 
|- ( T = <. A , B , C >. -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( 1st ` ( 1st ` T ) ) = A /\ ( 2nd ` ( 1st ` T ) ) = B /\ ( 2nd ` T ) = C ) ) )

Proof

Step Hyp Ref Expression
1 ot1stg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A )
2 ot2ndg 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )
3 ot3rdg 
 |-  ( C e. Z -> ( 2nd ` <. A , B , C >. ) = C )
4 3 3ad2ant3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( 2nd ` <. A , B , C >. ) = C )
5 1 2 4 3jca 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( 1st ` ( 1st ` <. A , B , C >. ) ) = A /\ ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B /\ ( 2nd ` <. A , B , C >. ) = C ) )
6 2fveq3 
 |-  ( T = <. A , B , C >. -> ( 1st ` ( 1st ` T ) ) = ( 1st ` ( 1st ` <. A , B , C >. ) ) )
7 6 eqeq1d 
 |-  ( T = <. A , B , C >. -> ( ( 1st ` ( 1st ` T ) ) = A <-> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A ) )
8 2fveq3 
 |-  ( T = <. A , B , C >. -> ( 2nd ` ( 1st ` T ) ) = ( 2nd ` ( 1st ` <. A , B , C >. ) ) )
9 8 eqeq1d 
 |-  ( T = <. A , B , C >. -> ( ( 2nd ` ( 1st ` T ) ) = B <-> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B ) )
10 fveqeq2 
 |-  ( T = <. A , B , C >. -> ( ( 2nd ` T ) = C <-> ( 2nd ` <. A , B , C >. ) = C ) )
11 7 9 10 3anbi123d 
 |-  ( T = <. A , B , C >. -> ( ( ( 1st ` ( 1st ` T ) ) = A /\ ( 2nd ` ( 1st ` T ) ) = B /\ ( 2nd ` T ) = C ) <-> ( ( 1st ` ( 1st ` <. A , B , C >. ) ) = A /\ ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B /\ ( 2nd ` <. A , B , C >. ) = C ) ) )
12 5 11 syl5ibr 
 |-  ( T = <. A , B , C >. -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( ( 1st ` ( 1st ` T ) ) = A /\ ( 2nd ` ( 1st ` T ) ) = B /\ ( 2nd ` T ) = C ) ) )