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