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	⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 )

Proof

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