Theorem dfacbasgrp

Description: A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988 . (Contributed by Stefan O'Rear, 9-Jul-2015)

	Ref	Expression
Assertion	dfacbasgrp	⊢ ( CHOICE ↔ ( Base “ Grp ) = ( V ∖ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		dfac10	⊢ ( CHOICE ↔ dom card = V )
2		basfn	⊢ Base Fn V
3		ssv	⊢ Grp ⊆ V
4		fvelimab	⊢ ( ( Base Fn V ∧ Grp ⊆ V ) → ( 𝑥 ∈ ( Base “ Grp ) ↔ ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 ) )
5	2 3 4	mp2an	⊢ ( 𝑥 ∈ ( Base “ Grp ) ↔ ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 )
6		eqid	⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
7	6	grpbn0	⊢ ( 𝑦 ∈ Grp → ( Base ‘ 𝑦 ) ≠ ∅ )
8		neeq1	⊢ ( ( Base ‘ 𝑦 ) = 𝑥 → ( ( Base ‘ 𝑦 ) ≠ ∅ ↔ 𝑥 ≠ ∅ ) )
9	7 8	syl5ibcom	⊢ ( 𝑦 ∈ Grp → ( ( Base ‘ 𝑦 ) = 𝑥 → 𝑥 ≠ ∅ ) )
10	9	rexlimiv	⊢ ( ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 → 𝑥 ≠ ∅ )
11	5 10	sylbi	⊢ ( 𝑥 ∈ ( Base “ Grp ) → 𝑥 ≠ ∅ )
12	11	adantl	⊢ ( ( dom card = V ∧ 𝑥 ∈ ( Base “ Grp ) ) → 𝑥 ≠ ∅ )
13		vex	⊢ 𝑥 ∈ V
14	12 13	jctil	⊢ ( ( dom card = V ∧ 𝑥 ∈ ( Base “ Grp ) ) → ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) )
15		ablgrp	⊢ ( 𝑥 ∈ Abel → 𝑥 ∈ Grp )
16	15	ssriv	⊢ Abel ⊆ Grp
17		imass2	⊢ ( Abel ⊆ Grp → ( Base “ Abel ) ⊆ ( Base “ Grp ) )
18	16 17	ax-mp	⊢ ( Base “ Abel ) ⊆ ( Base “ Grp )
19		simprl	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ V )
20		simpl	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → dom card = V )
21	19 20	eleqtrrd	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ dom card )
22		simprr	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ≠ ∅ )
23		isnumbasgrplem3	⊢ ( ( 𝑥 ∈ dom card ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( Base “ Abel ) )
24	21 22 23	syl2anc	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( Base “ Abel ) )
25	18 24	sselid	⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( Base “ Grp ) )
26	14 25	impbida	⊢ ( dom card = V → ( 𝑥 ∈ ( Base “ Grp ) ↔ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) )
27		eldifsn	⊢ ( 𝑥 ∈ ( V ∖ { ∅ } ) ↔ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) )
28	26 27	bitr4di	⊢ ( dom card = V → ( 𝑥 ∈ ( Base “ Grp ) ↔ 𝑥 ∈ ( V ∖ { ∅ } ) ) )
29	28	eqrdv	⊢ ( dom card = V → ( Base “ Grp ) = ( V ∖ { ∅ } ) )
30		fvex	⊢ ( har ‘ 𝑥 ) ∈ V
31	13 30	unex	⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ V
32		ssun2	⊢ ( har ‘ 𝑥 ) ⊆ ( 𝑥 ∪ ( har ‘ 𝑥 ) )
33		harn0	⊢ ( 𝑥 ∈ V → ( har ‘ 𝑥 ) ≠ ∅ )
34	13 33	ax-mp	⊢ ( har ‘ 𝑥 ) ≠ ∅
35		ssn0	⊢ ( ( ( har ‘ 𝑥 ) ⊆ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∧ ( har ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅ )
36	32 34 35	mp2an	⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅
37		eldifsn	⊢ ( ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } ) ↔ ( ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ V ∧ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅ ) )
38	31 36 37	mpbir2an	⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } )
39	38	a1i	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } ) )
40		id	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( Base “ Grp ) = ( V ∖ { ∅ } ) )
41	39 40	eleqtrrd	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( Base “ Grp ) )
42		isnumbasgrp	⊢ ( 𝑥 ∈ dom card ↔ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( Base “ Grp ) )
43	41 42	sylibr	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → 𝑥 ∈ dom card )
44	13	a1i	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → 𝑥 ∈ V )
45	43 44	2thd	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∈ dom card ↔ 𝑥 ∈ V ) )
46	45	eqrdv	⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → dom card = V )
47	29 46	impbii	⊢ ( dom card = V ↔ ( Base “ Grp ) = ( V ∖ { ∅ } ) )
48	1 47	bitri	⊢ ( CHOICE ↔ ( Base “ Grp ) = ( V ∖ { ∅ } ) )