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

Metamath Proof Explorer

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