This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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