Metamath Proof Explorer

Theorem elxpxpss

Description: Version of elrel for triple cross products. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Assertion elxpxpss 
|- ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> E. x E. y E. z A = <. <. x , y >. , z >. )

Proof

Step Hyp Ref Expression
1 ssel2 
 |-  ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> A e. ( ( B X. C ) X. D ) )
2 elxpxp 
 |-  ( A e. ( ( B X. C ) X. D ) <-> E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. )
3 rexex 
 |-  ( E. z e. D A = <. <. x , y >. , z >. -> E. z A = <. <. x , y >. , z >. )
4 3 reximi 
 |-  ( E. y e. C E. z e. D A = <. <. x , y >. , z >. -> E. y e. C E. z A = <. <. x , y >. , z >. )
5 rexex 
 |-  ( E. y e. C E. z A = <. <. x , y >. , z >. -> E. y E. z A = <. <. x , y >. , z >. )
6 4 5 syl 
 |-  ( E. y e. C E. z e. D A = <. <. x , y >. , z >. -> E. y E. z A = <. <. x , y >. , z >. )
7 6 reximi 
 |-  ( E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. -> E. x e. B E. y E. z A = <. <. x , y >. , z >. )
8 rexex 
 |-  ( E. x e. B E. y E. z A = <. <. x , y >. , z >. -> E. x E. y E. z A = <. <. x , y >. , z >. )
9 7 8 syl 
 |-  ( E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. -> E. x E. y E. z A = <. <. x , y >. , z >. )
10 2 9 sylbi 
 |-  ( A e. ( ( B X. C ) X. D ) -> E. x E. y E. z A = <. <. x , y >. , z >. )
11 1 10 syl 
 |-  ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> E. x E. y E. z A = <. <. x , y >. , z >. )