This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpdom2g

Description: Dominance law for Cartesian product. Theorem 6L(c) of Enderton p. 149. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion xpdom2g 
|- ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( C X. B ) )

Proof

Step Hyp Ref Expression
1 xpeq1 
 |-  ( x = C -> ( x X. A ) = ( C X. A ) )
2 xpeq1 
 |-  ( x = C -> ( x X. B ) = ( C X. B ) )
3 1 2 breq12d 
 |-  ( x = C -> ( ( x X. A ) ~<_ ( x X. B ) <-> ( C X. A ) ~<_ ( C X. B ) ) )
4 3 imbi2d 
 |-  ( x = C -> ( ( A ~<_ B -> ( x X. A ) ~<_ ( x X. B ) ) <-> ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) ) ) )
5 vex 
 |-  x e. _V
6 5 xpdom2 
 |-  ( A ~<_ B -> ( x X. A ) ~<_ ( x X. B ) )
7 4 6 vtoclg 
 |-  ( C e. V -> ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) ) )
8 7 imp 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( C X. B ) )