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

Metamath Proof Explorer

Theorem djudom2

Description: Ordering law for cardinal addition. Theorem 6L(a) of Enderton p. 149. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion djudom2 ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐶 ⊔ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 djudom1 ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ⊔ 𝐶 ) ≼ ( 𝐵 ⊔ 𝐶 ) )
2 reldom ⊢ Rel ≼
3 2 brrelex1i ⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
4 djucomen ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐴 ) )
5 3 4 sylan ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐴 ) )
6 2 brrelex2i ⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
7 djucomen ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐵 ) )
8 6 7 sylan ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐵 ) )
9 domen1 ⊢ ( ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐴 ) → ( ( 𝐴 ⊔ 𝐶 ) ≼ ( 𝐵 ⊔ 𝐶 ) ↔ ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐵 ⊔ 𝐶 ) ) )
10 domen2 ⊢ ( ( 𝐵 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐵 ) → ( ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐵 ⊔ 𝐶 ) ↔ ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐶 ⊔ 𝐵 ) ) )
11 9 10 sylan9bb ⊢ ( ( ( 𝐴 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐴 ) ∧ ( 𝐵 ⊔ 𝐶 ) ≈ ( 𝐶 ⊔ 𝐵 ) ) → ( ( 𝐴 ⊔ 𝐶 ) ≼ ( 𝐵 ⊔ 𝐶 ) ↔ ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐶 ⊔ 𝐵 ) ) )
12 5 8 11 syl2anc ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐴 ⊔ 𝐶 ) ≼ ( 𝐵 ⊔ 𝐶 ) ↔ ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐶 ⊔ 𝐵 ) ) )
13 1 12 mpbid ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐶 ⊔ 𝐴 ) ≼ ( 𝐶 ⊔ 𝐵 ) )