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