Metamath Proof Explorer

Theorem isnumbasabl

Description: A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015)

		Ref	Expression
	Assertion	isnumbasabl	$⊢ S \in dom card \leftrightarrow S \cup har (S) \in Base [Abel]$

Proof

Step	Hyp	Ref	Expression
1		harcl	$⊢ har (S) \in On$
2		onenon	$⊢ har (S) \in On \to har (S) \in dom card$
3	1 2	ax-mp	$⊢ har (S) \in dom card$
4		unnum	$⊢ (S \in dom card \land har (S) \in dom card) \to S \cup har (S) \in dom card$
5	3 4	mpan2	$⊢ S \in dom card \to S \cup har (S) \in dom card$
6		ssun2	$⊢ har (S) \subseteq S \cup har (S)$
7		harn0	$⊢ S \in dom card \to har (S) \neq \emptyset$
8		ssn0	$⊢ (har (S) \subseteq S \cup har (S) \land har (S) \neq \emptyset) \to S \cup har (S) \neq \emptyset$
9	6 7 8	sylancr	$⊢ S \in dom card \to S \cup har (S) \neq \emptyset$
10		isnumbasgrplem3	$⊢ (S \cup har (S) \in dom card \land S \cup har (S) \neq \emptyset) \to S \cup har (S) \in Base [Abel]$
11	5 9 10	syl2anc	$⊢ S \in dom card \to S \cup har (S) \in Base [Abel]$
12		ablgrp	$⊢ x \in Abel \to x \in Grp$
13	12	ssriv	$⊢ Abel \subseteq Grp$
14		imass2	$⊢ Abel \subseteq Grp \to Base [Abel] \subseteq Base [Grp]$
15	13 14	ax-mp	$⊢ Base [Abel] \subseteq Base [Grp]$
16	15	sseli	$⊢ S \cup har (S) \in Base [Abel] \to S \cup har (S) \in Base [Grp]$
17		isnumbasgrplem2	$⊢ S \cup har (S) \in Base [Grp] \to S \in dom card$
18	16 17	syl	$⊢ S \cup har (S) \in Base [Abel] \to S \in dom card$
19	11 18	impbii	$⊢ S \in dom card \leftrightarrow S \cup har (S) \in Base [Abel]$