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 ) )