Metamath Proof Explorer

Theorem otel3xp

Description: An ordered triple is an element of a doubled Cartesian product. (Contributed by Alexander van der Vekens, 26-Feb-2018)

Ref Expression
Assertion otel3xp 
|- ( ( T = <. A , B , C >. /\ ( A e. X /\ B e. Y /\ C e. Z ) ) -> T e. ( ( X X. Y ) X. Z ) )

Proof

Step Hyp Ref Expression
1 df-ot 
 |-  <. A , B , C >. = <. <. A , B >. , C >.
2 3simpa 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> ( A e. X /\ B e. Y ) )
3 opelxp 
 |-  ( <. A , B >. e. ( X X. Y ) <-> ( A e. X /\ B e. Y ) )
4 2 3 sylibr 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> <. A , B >. e. ( X X. Y ) )
5 simp3 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> C e. Z )
6 4 5 opelxpd 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> <. <. A , B >. , C >. e. ( ( X X. Y ) X. Z ) )
7 1 6 eqeltrid 
 |-  ( ( A e. X /\ B e. Y /\ C e. Z ) -> <. A , B , C >. e. ( ( X X. Y ) X. Z ) )
8 eleq1 
 |-  ( T = <. A , B , C >. -> ( T e. ( ( X X. Y ) X. Z ) <-> <. A , B , C >. e. ( ( X X. Y ) X. Z ) ) )
9 7 8 syl5ibr 
 |-  ( T = <. A , B , C >. -> ( ( A e. X /\ B e. Y /\ C e. Z ) -> T e. ( ( X X. Y ) X. Z ) ) )
10 9 imp 
 |-  ( ( T = <. A , B , C >. /\ ( A e. X /\ B e. Y /\ C e. Z ) ) -> T e. ( ( X X. Y ) X. Z ) )