Theorem djudom1

Description: Ordering law for cardinal addition. Exercise 4.56(f) of Mendelson p. 258. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 1-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { ∅ } ∈ V
2	1	xpdom2	⊢ ( 𝐴 ≼ 𝐵 → ( { ∅ } × 𝐴 ) ≼ ( { ∅ } × 𝐵 ) )
3		snex	⊢ { 1o } ∈ V
4		xpexg	⊢ ( ( { 1o } ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( { 1o } × 𝐶 ) ∈ V )
5	3 4	mpan	⊢ ( 𝐶 ∈ 𝑉 → ( { 1o } × 𝐶 ) ∈ V )
6		domrefg	⊢ ( ( { 1o } × 𝐶 ) ∈ V → ( { 1o } × 𝐶 ) ≼ ( { 1o } × 𝐶 ) )
7	5 6	syl	⊢ ( 𝐶 ∈ 𝑉 → ( { 1o } × 𝐶 ) ≼ ( { 1o } × 𝐶 ) )
8		xp01disjl	⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅
9		undom	⊢ ( ( ( ( { ∅ } × 𝐴 ) ≼ ( { ∅ } × 𝐵 ) ∧ ( { 1o } × 𝐶 ) ≼ ( { 1o } × 𝐶 ) ) ∧ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≼ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
10	8 9	mpan2	⊢ ( ( ( { ∅ } × 𝐴 ) ≼ ( { ∅ } × 𝐵 ) ∧ ( { 1o } × 𝐶 ) ≼ ( { 1o } × 𝐶 ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≼ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
11	2 7 10	syl2an	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) ) ≼ ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
12		df-dju	⊢ ( 𝐴 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐶 ) )
13		df-dju	⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) )
14	11 12 13	3brtr4g	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ⊔ 𝐶 ) ≼ ( 𝐵 ⊔ 𝐶 ) )