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 \in dom card \land ω ≼ A \land B ≼ A) \to (A \cup B) \approx A$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to A \in dom card$
2		reldom	$⊢ Rel ≼$
3	2	brrelex1i	$⊢ B ≼ A \to B \in V$
4	3	3ad2ant3	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to B \in V$
5		undjudom	$⊢ (A \in dom card \land B \in V) \to (A \cup B) ≼ (A ⊔︀ B)$
6	1 4 5	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \cup B) ≼ (A ⊔︀ B)$
7		infdjuabs	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A ⊔︀ B) \approx A$
8		domentr	$⊢ ((A \cup B) ≼ (A ⊔︀ B) \land (A ⊔︀ B) \approx A) \to (A \cup B) ≼ A$
9	6 7 8	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \cup B) ≼ A$
10		unexg	$⊢ (A \in dom card \land B \in V) \to A \cup B \in V$
11	1 4 10	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to A \cup B \in V$
12		ssun1	$⊢ A \subseteq A \cup B$
13		ssdomg	$⊢ A \cup B \in V \to (A \subseteq A \cup B \to A ≼ (A \cup B))$
14	11 12 13	mpisyl	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to A ≼ (A \cup B)$
15		sbth	$⊢ ((A \cup B) ≼ A \land A ≼ (A \cup B)) \to (A \cup B) \approx A$
16	9 14 15	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \cup B) \approx A$