Theorem isnumbasgrp

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

	Ref	Expression
Assertion	isnumbasgrp	|- ( S e. dom card <-> ( S u. ( har ` S ) ) e. ( Base " Grp ) )

Proof

Step	Hyp	Ref	Expression
1		ablgrp	|- ( x e. Abel -> x e. Grp )
2	1	ssriv	|- Abel C_ Grp
3		imass2	|- ( Abel C_ Grp -> ( Base " Abel ) C_ ( Base " Grp ) )
4	2 3	ax-mp	|- ( Base " Abel ) C_ ( Base " Grp )
5		isnumbasabl	|- ( S e. dom card <-> ( S u. ( har ` S ) ) e. ( Base " Abel ) )
6	5	biimpi	|- ( S e. dom card -> ( S u. ( har ` S ) ) e. ( Base " Abel ) )
7	4 6	sselid	|- ( S e. dom card -> ( S u. ( har ` S ) ) e. ( Base " Grp ) )
8		isnumbasgrplem2	|- ( ( S u. ( har ` S ) ) e. ( Base " Grp ) -> S e. dom card )
9	7 8	impbii	|- ( S e. dom card <-> ( S u. ( har ` S ) ) e. ( Base " Grp ) )