Theorem isnumbasabl

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

	Ref	Expression
Assertion	isnumbasabl	⊢ ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )

Proof

Step	Hyp	Ref	Expression
1		harcl	⊢ ( har ‘ 𝑆 ) ∈ On
2		onenon	⊢ ( ( har ‘ 𝑆 ) ∈ On → ( har ‘ 𝑆 ) ∈ dom card )
3	1 2	ax-mp	⊢ ( har ‘ 𝑆 ) ∈ dom card
4		unnum	⊢ ( ( 𝑆 ∈ dom card ∧ ( har ‘ 𝑆 ) ∈ dom card ) → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ dom card )
5	3 4	mpan2	⊢ ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ dom card )
6		ssun2	⊢ ( har ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( har ‘ 𝑆 ) )
7		harn0	⊢ ( 𝑆 ∈ dom card → ( har ‘ 𝑆 ) ≠ ∅ )
8		ssn0	⊢ ( ( ( har ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∧ ( har ‘ 𝑆 ) ≠ ∅ ) → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ≠ ∅ )
9	6 7 8	sylancr	⊢ ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ≠ ∅ )
10		isnumbasgrplem3	⊢ ( ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ dom card ∧ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ≠ ∅ ) → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )
11	5 9 10	syl2anc	⊢ ( 𝑆 ∈ dom card → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )
12		ablgrp	⊢ ( 𝑥 ∈ Abel → 𝑥 ∈ Grp )
13	12	ssriv	⊢ Abel ⊆ Grp
14		imass2	⊢ ( Abel ⊆ Grp → ( Base “ Abel ) ⊆ ( Base “ Grp ) )
15	13 14	ax-mp	⊢ ( Base “ Abel ) ⊆ ( Base “ Grp )
16	15	sseli	⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) → ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) )
17		isnumbasgrplem2	⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) → 𝑆 ∈ dom card )
18	16 17	syl	⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) → 𝑆 ∈ dom card )
19	11 18	impbii	⊢ ( 𝑆 ∈ dom card ↔ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Abel ) )