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	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 × 𝐴 ) = ( 𝐶 × 𝐴 ) )
2		xpeq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 × 𝐵 ) = ( 𝐶 × 𝐵 ) )
3	1 2	breq12d	⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 × 𝐴 ) ≼ ( 𝑥 × 𝐵 ) ↔ ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) ) )
4	3	imbi2d	⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ≼ 𝐵 → ( 𝑥 × 𝐴 ) ≼ ( 𝑥 × 𝐵 ) ) ↔ ( 𝐴 ≼ 𝐵 → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) ) ) )
5		vex	⊢ 𝑥 ∈ V
6	5	xpdom2	⊢ ( 𝐴 ≼ 𝐵 → ( 𝑥 × 𝐴 ) ≼ ( 𝑥 × 𝐵 ) )
7	4 6	vtoclg	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐴 ≼ 𝐵 → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) ) )
8	7	imp	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) )