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 ⊢ C ∈ V ∧ A ≼ B → A × C ≼ B × C

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ⁡ ≼
2 1 brrelex1i ⊢ A ≼ B → A ∈ V
3 xpcomeng ⊢ A ∈ V ∧ C ∈ V → A × C ≈ C × A
4 3 ancoms ⊢ C ∈ V ∧ A ∈ V → A × C ≈ C × A
5 2 4 sylan2 ⊢ C ∈ V ∧ A ≼ B → A × C ≈ C × A
6 xpdom2g ⊢ C ∈ V ∧ A ≼ B → C × A ≼ C × B
7 1 brrelex2i ⊢ A ≼ B → B ∈ V
8 xpcomeng ⊢ C ∈ V ∧ B ∈ V → C × B ≈ B × C
9 7 8 sylan2 ⊢ C ∈ V ∧ A ≼ B → C × B ≈ B × C
10 domentr ⊢ C × A ≼ C × B ∧ C × B ≈ B × C → C × A ≼ B × C
11 6 9 10 syl2anc ⊢ C ∈ V ∧ A ≼ B → C × A ≼ B × C
12 endomtr ⊢ A × C ≈ C × A ∧ C × A ≼ B × C → A × C ≼ B × C
13 5 11 12 syl2anc ⊢ C ∈ V ∧ A ≼ B → A × C ≼ B × C