Theorem xpdom1g

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

	Ref	Expression
Assertion	xpdom1g	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$

Proof

Step	Hyp	Ref	Expression
1		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2	1	brrelex1i	$$⊢A\preccurlyeq B\to A\in \mathrm{V}$$
3		xpcomeng	$$⊢\left(A\in \mathrm{V}\wedge C\in V\right)\to \left(A\times C\right)\approx \left(C\times A\right)$$
4	3	ancoms	$$⊢\left(C\in V\wedge A\in \mathrm{V}\right)\to \left(A\times C\right)\approx \left(C\times A\right)$$
5	2 4	sylan2	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(A\times C\right)\approx \left(C\times A\right)$$
6		xpdom2g	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(C\times A\right)\preccurlyeq \left(C\times B\right)$$
7	1	brrelex2i	$$⊢A\preccurlyeq B\to B\in \mathrm{V}$$
8		xpcomeng	$$⊢\left(C\in V\wedge B\in \mathrm{V}\right)\to \left(C\times B\right)\approx \left(B\times C\right)$$
9	7 8	sylan2	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(C\times B\right)\approx \left(B\times C\right)$$
10		domentr	$$⊢\left(\left(C\times A\right)\preccurlyeq \left(C\times B\right)\wedge \left(C\times B\right)\approx \left(B\times C\right)\right)\to \left(C\times A\right)\preccurlyeq \left(B\times C\right)$$
11	6 9 10	syl2anc	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(C\times A\right)\preccurlyeq \left(B\times C\right)$$
12		endomtr	$$⊢\left(\left(A\times C\right)\approx \left(C\times A\right)\wedge \left(C\times A\right)\preccurlyeq \left(B\times C\right)\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$
13	5 11 12	syl2anc	$$⊢\left(C\in V\wedge A\preccurlyeq B\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$