Metamath Proof Explorer

Theorem infdju

Description: The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infdju ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 unnum ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )
3 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
4 ssdomg ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ dom card → ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) ) )
5 2 3 4 mpisyl ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) )
6 simp1 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ∈ dom card )
7 djudom2 ⊢ ( ( 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) ∧ 𝐴 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) )
8 5 6 7 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) )
9 djucomen ⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝐴 ∪ 𝐵 ) ∈ dom card ) → ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) ≈ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) )
10 6 2 9 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) ≈ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) )
11 domentr ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) ∧ ( 𝐴 ⊔ ( 𝐴 ∪ 𝐵 ) ) ≈ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) )
12 8 10 11 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) )
13 simp3 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ≼ 𝐴 )
14 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
15 ssdomg ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ dom card → ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ) )
16 2 14 15 mpisyl ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) )
17 domtr ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ) → ω ≼ ( 𝐴 ∪ 𝐵 ) )
18 13 16 17 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ≼ ( 𝐴 ∪ 𝐵 ) )
19 infdjuabs ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ dom card ∧ ω ≼ ( 𝐴 ∪ 𝐵 ) ∧ 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ) → ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) )
20 2 18 16 19 syl3anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) )
21 domentr ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊔ 𝐴 ) ≈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ∪ 𝐵 ) )
22 12 20 21 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ∪ 𝐵 ) )
23 undjudom ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
24 23 3adant3 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
25 sbth ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )
26 22 24 25 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ 𝐵 ) )