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\in \mathrm{dom}\mathrm{card}\leftrightarrow S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Grp}\right]$$

Proof

Step	Hyp	Ref	Expression
1		ablgrp	$$⊢x\in \mathrm{Abel}\to x\in \mathrm{Grp}$$
2	1	ssriv	$$⊢\mathrm{Abel}\subseteq \mathrm{Grp}$$
3		imass2	$$⊢\mathrm{Abel}\subseteq \mathrm{Grp}\to \mathrm{Base}\left[\mathrm{Abel}\right]\subseteq \mathrm{Base}\left[\mathrm{Grp}\right]$$
4	2 3	ax-mp	$$⊢\mathrm{Base}\left[\mathrm{Abel}\right]\subseteq \mathrm{Base}\left[\mathrm{Grp}\right]$$
5		isnumbasabl	$$⊢S\in \mathrm{dom}\mathrm{card}\leftrightarrow S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Abel}\right]$$
6	5	biimpi	$$⊢S\in \mathrm{dom}\mathrm{card}\to S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Abel}\right]$$
7	4 6	sselid	$$⊢S\in \mathrm{dom}\mathrm{card}\to S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Grp}\right]$$
8		isnumbasgrplem2	$$⊢S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Grp}\right]\to S\in \mathrm{dom}\mathrm{card}$$
9	7 8	impbii	$$⊢S\in \mathrm{dom}\mathrm{card}\leftrightarrow S\cup \mathrm{har}\left(S\right)\in \mathrm{Base}\left[\mathrm{Grp}\right]$$