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

### Proof

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