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

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
3		xpcomeng	⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐶 × 𝐴 ) )
4	3	ancoms	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐶 × 𝐴 ) )
5	2 4	sylan2	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐶 × 𝐴 ) )
6		xpdom2g	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) )
7	1	brrelex2i	⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
8		xpcomeng	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ∈ V ) → ( 𝐶 × 𝐵 ) ≈ ( 𝐵 × 𝐶 ) )
9	7 8	sylan2	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐶 × 𝐵 ) ≈ ( 𝐵 × 𝐶 ) )
10		domentr	⊢ ( ( ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) ∧ ( 𝐶 × 𝐵 ) ≈ ( 𝐵 × 𝐶 ) ) → ( 𝐶 × 𝐴 ) ≼ ( 𝐵 × 𝐶 ) )
11	6 9 10	syl2anc	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐶 × 𝐴 ) ≼ ( 𝐵 × 𝐶 ) )
12		endomtr	⊢ ( ( ( 𝐴 × 𝐶 ) ≈ ( 𝐶 × 𝐴 ) ∧ ( 𝐶 × 𝐴 ) ≼ ( 𝐵 × 𝐶 ) ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐶 ) )
13	5 11 12	syl2anc	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 × 𝐶 ) ≼ ( 𝐵 × 𝐶 ) )