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

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