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 e. dom card <-> ( S u. ( har ` S ) ) e. ( Base " Abel ) )

Proof

Step	Hyp	Ref	Expression
1		harcl	|- ( har ` S ) e. On
2		onenon	|- ( ( har ` S ) e. On -> ( har ` S ) e. dom card )
3	1 2	ax-mp	|- ( har ` S ) e. dom card
4		unnum	|- ( ( S e. dom card /\ ( har ` S ) e. dom card ) -> ( S u. ( har ` S ) ) e. dom card )
5	3 4	mpan2	|- ( S e. dom card -> ( S u. ( har ` S ) ) e. dom card )
6		ssun2	|- ( har ` S ) C_ ( S u. ( har ` S ) )
7		harn0	|- ( S e. dom card -> ( har ` S ) =/= (/) )
8		ssn0	|- ( ( ( har ` S ) C_ ( S u. ( har ` S ) ) /\ ( har ` S ) =/= (/) ) -> ( S u. ( har ` S ) ) =/= (/) )
9	6 7 8	sylancr	|- ( S e. dom card -> ( S u. ( har ` S ) ) =/= (/) )
10		isnumbasgrplem3	|- ( ( ( S u. ( har ` S ) ) e. dom card /\ ( S u. ( har ` S ) ) =/= (/) ) -> ( S u. ( har ` S ) ) e. ( Base " Abel ) )
11	5 9 10	syl2anc	|- ( S e. dom card -> ( S u. ( har ` S ) ) e. ( Base " Abel ) )
12		ablgrp	|- ( x e. Abel -> x e. Grp )
13	12	ssriv	|- Abel C_ Grp
14		imass2	|- ( Abel C_ Grp -> ( Base " Abel ) C_ ( Base " Grp ) )
15	13 14	ax-mp	|- ( Base " Abel ) C_ ( Base " Grp )
16	15	sseli	|- ( ( S u. ( har ` S ) ) e. ( Base " Abel ) -> ( S u. ( har ` S ) ) e. ( Base " Grp ) )
17		isnumbasgrplem2	|- ( ( S u. ( har ` S ) ) e. ( Base " Grp ) -> S e. dom card )
18	16 17	syl	|- ( ( S u. ( har ` S ) ) e. ( Base " Abel ) -> S e. dom card )
19	11 18	impbii	|- ( S e. dom card <-> ( S u. ( har ` S ) ) e. ( Base " Abel ) )