Metamath Proof Explorer


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 dom card S har S Base Grp

Proof

Step Hyp Ref Expression
1 ablgrp x Abel x Grp
2 1 ssriv Abel Grp
3 imass2 Abel Grp Base Abel Base Grp
4 2 3 ax-mp Base Abel Base Grp
5 isnumbasabl S dom card S har S Base Abel
6 5 biimpi S dom card S har S Base Abel
7 4 6 sseldi S dom card S har S Base Grp
8 isnumbasgrplem2 S har S Base Grp S dom card
9 7 8 impbii S dom card S har S Base Grp