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

Proof

Step Hyp Ref Expression
1 djudom1 ⊢ A ≼ B ∧ C ∈ V → A ⊔︀ C ≼ B ⊔︀ C
2 reldom ⊢ Rel ⁡ ≼
3 2 brrelex1i ⊢ A ≼ B → A ∈ V
4 djucomen ⊢ A ∈ V ∧ C ∈ V → A ⊔︀ C ≈ C ⊔︀ A
5 3 4 sylan ⊢ A ≼ B ∧ C ∈ V → A ⊔︀ C ≈ C ⊔︀ A
6 2 brrelex2i ⊢ A ≼ B → B ∈ V
7 djucomen ⊢ B ∈ V ∧ C ∈ V → B ⊔︀ C ≈ C ⊔︀ B
8 6 7 sylan ⊢ A ≼ B ∧ C ∈ V → B ⊔︀ C ≈ C ⊔︀ B
9 domen1 ⊢ A ⊔︀ C ≈ C ⊔︀ A → A ⊔︀ C ≼ B ⊔︀ C ↔ C ⊔︀ A ≼ B ⊔︀ C
10 domen2 ⊢ B ⊔︀ C ≈ C ⊔︀ B → C ⊔︀ A ≼ B ⊔︀ C ↔ C ⊔︀ A ≼ C ⊔︀ B
11 9 10 sylan9bb ⊢ A ⊔︀ C ≈ C ⊔︀ A ∧ B ⊔︀ C ≈ C ⊔︀ B → A ⊔︀ C ≼ B ⊔︀ C ↔ C ⊔︀ A ≼ C ⊔︀ B
12 5 8 11 syl2anc ⊢ A ≼ B ∧ C ∈ V → A ⊔︀ C ≼ B ⊔︀ C ↔ C ⊔︀ A ≼ C ⊔︀ B
13 1 12 mpbid ⊢ A ≼ B ∧ C ∈ V → C ⊔︀ A ≼ C ⊔︀ B