Metamath Proof Explorer

Theorem infunabs

Description: An infinite set is equinumerous to its union with a smaller one. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infunabs ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∪ B ≈ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∈ dom ⁡ card
2 reldom ⊢ Rel ⁡ ≼
3 2 brrelex1i ⊢ B ≼ A → B ∈ V
4 3 3ad2ant3 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → B ∈ V
5 undjudom ⊢ A ∈ dom ⁡ card ∧ B ∈ V → A ∪ B ≼ A ⊔︀ B
6 1 4 5 syl2anc ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∪ B ≼ A ⊔︀ B
7 infdjuabs ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ⊔︀ B ≈ A
8 domentr ⊢ A ∪ B ≼ A ⊔︀ B ∧ A ⊔︀ B ≈ A → A ∪ B ≼ A
9 6 7 8 syl2anc ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∪ B ≼ A
10 unexg ⊢ A ∈ dom ⁡ card ∧ B ∈ V → A ∪ B ∈ V
11 1 4 10 syl2anc ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∪ B ∈ V
12 ssun1 ⊢ A ⊆ A ∪ B
13 ssdomg ⊢ A ∪ B ∈ V → A ⊆ A ∪ B → A ≼ A ∪ B
14 11 12 13 mpisyl ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ≼ A ∪ B
15 sbth ⊢ A ∪ B ≼ A ∧ A ≼ A ∪ B → A ∪ B ≈ A
16 9 14 15 syl2anc ⊢ A ∈ dom ⁡ card ∧ ω ≼ A ∧ B ≼ A → A ∪ B ≈ A