Metamath Proof Explorer

Theorem bj-xpcossxp

Description: The composition of two Cartesian products is included in the expected Cartesian product. There is equality if ( B i^i C ) =/= (/) , see xpcogend . (Contributed by BJ, 22-May-2024)

Ref Expression
Assertion bj-xpcossxp 
|- ( ( C X. D ) o. ( A X. B ) ) C_ ( A X. D )

Proof

Step Hyp Ref Expression
1 brxp 
 |-  ( x ( A X. B ) y <-> ( x e. A /\ y e. B ) )
2 brxp 
 |-  ( y ( C X. D ) t <-> ( y e. C /\ t e. D ) )
3 1 2 anbi12i 
 |-  ( ( x ( A X. B ) y /\ y ( C X. D ) t ) <-> ( ( x e. A /\ y e. B ) /\ ( y e. C /\ t e. D ) ) )
4 an43 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( y e. C /\ t e. D ) ) <-> ( ( x e. A /\ t e. D ) /\ ( y e. B /\ y e. C ) ) )
5 3 4 bitri 
 |-  ( ( x ( A X. B ) y /\ y ( C X. D ) t ) <-> ( ( x e. A /\ t e. D ) /\ ( y e. B /\ y e. C ) ) )
6 5 exbii 
 |-  ( E. y ( x ( A X. B ) y /\ y ( C X. D ) t ) <-> E. y ( ( x e. A /\ t e. D ) /\ ( y e. B /\ y e. C ) ) )
7 19.42v 
 |-  ( E. y ( ( x e. A /\ t e. D ) /\ ( y e. B /\ y e. C ) ) <-> ( ( x e. A /\ t e. D ) /\ E. y ( y e. B /\ y e. C ) ) )
8 7 simplbi 
 |-  ( E. y ( ( x e. A /\ t e. D ) /\ ( y e. B /\ y e. C ) ) -> ( x e. A /\ t e. D ) )
9 6 8 sylbi 
 |-  ( E. y ( x ( A X. B ) y /\ y ( C X. D ) t ) -> ( x e. A /\ t e. D ) )
10 9 ssopab2i 
 |-  { <. x , t >. | E. y ( x ( A X. B ) y /\ y ( C X. D ) t ) } C_ { <. x , t >. | ( x e. A /\ t e. D ) }
11 df-co 
 |-  ( ( C X. D ) o. ( A X. B ) ) = { <. x , t >. | E. y ( x ( A X. B ) y /\ y ( C X. D ) t ) }
12 df-xp 
 |-  ( A X. D ) = { <. x , t >. | ( x e. A /\ t e. D ) }
13 10 11 12 3sstr4i 
 |-  ( ( C X. D ) o. ( A X. B ) ) C_ ( A X. D )