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 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card ∧ ω ≼ A → A ⊔︀ B ≈ A ∪ B

Proof

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