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	sseldi	⊢ ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )
8		isnumbasgrplem2	⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) → 𝑆 ∈ dom card )
9	7 8	impbii	⊢ ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )