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	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(C\times A\right)\preccurlyeq \left(C\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢x=C\to x\times A=C\times A$$
2		xpeq1	$$⊢x=C\to x\times B=C\times B$$
3	1 2	breq12d	$$⊢x=C\to \left(\left(x\times A\right)\preccurlyeq \left(x\times B\right)\leftrightarrow \left(C\times A\right)\preccurlyeq \left(C\times B\right)\right)$$
4	3	imbi2d	$$⊢x=C\to \left(\left(A\preccurlyeq B\to \left(x\times A\right)\preccurlyeq \left(x\times B\right)\right)\leftrightarrow \left(A\preccurlyeq B\to \left(C\times A\right)\preccurlyeq \left(C\times B\right)\right)\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	xpdom2	$$⊢A\preccurlyeq B\to \left(x\times A\right)\preccurlyeq \left(x\times B\right)$$
7	4 6	vtoclg	$$⊢C\in V\to \left(A\preccurlyeq B\to \left(C\times A\right)\preccurlyeq \left(C\times B\right)\right)$$
8	7	imp	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(C\times A\right)\preccurlyeq \left(C\times B\right)$$