Metamath Proof Explorer

Theorem ot1st2nd

Description: Reconstruction of a member of a nested Cartesian product in terms of its ordered triple components. (Contributed by BTernaryTau, 9-Oct-2026)

Ref Expression
Assertion ot1st2nd 
|- ( A e. ( ( B X. C ) X. D ) -> A = <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) , ( 2nd ` A ) >. )

Proof

Step Hyp Ref Expression
1 1st2nd2 
 |-  ( A e. ( ( B X. C ) X. D ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2 xp1st 
 |-  ( A e. ( ( B X. C ) X. D ) -> ( 1st ` A ) e. ( B X. C ) )
3 1st2nd2 
 |-  ( ( 1st ` A ) e. ( B X. C ) -> ( 1st ` A ) = <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. )
4 2 3 syl 
 |-  ( A e. ( ( B X. C ) X. D ) -> ( 1st ` A ) = <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. )
5 4 opeq1d 
 |-  ( A e. ( ( B X. C ) X. D ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
6 1 5 eqtrd 
 |-  ( A e. ( ( B X. C ) X. D ) -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
7 df-ot 
 |-  <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) , ( 2nd ` A ) >. = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >.
8 6 7 eqtr4di 
 |-  ( A e. ( ( B X. C ) X. D ) -> A = <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) , ( 2nd ` A ) >. )