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 ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )

Proof

Step Hyp Ref Expression
1 ablgrp ( 𝑥 ∈ Abel → 𝑥 ∈ 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 ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )
6 5 biimpi ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )
7 4 6 sselid ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )
8 isnumbasgrplem2 ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) → 𝑆 ∈ dom card )
9 7 8 impbii ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )