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 \leftrightarrow Base [Grp] = V ∖ \{\emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		dfac10	$⊢ CHOICE \leftrightarrow dom card = V$
2		basfn	$⊢ Base Fn V$
3		ssv	$⊢ Grp \subseteq V$
4		fvelimab	$⊢ (Base Fn V \land Grp \subseteq V) \to (x \in Base [Grp] \leftrightarrow \exists y \in Grp {Base}_{y} = x)$
5	2 3 4	mp2an	$⊢ x \in Base [Grp] \leftrightarrow \exists y \in Grp {Base}_{y} = x$
6		eqid	$⊢ {Base}_{y} = {Base}_{y}$
7	6	grpbn0	$⊢ y \in Grp \to {Base}_{y} \neq \emptyset$
8		neeq1	$⊢ {Base}_{y} = x \to ({Base}_{y} \neq \emptyset \leftrightarrow x \neq \emptyset)$
9	7 8	syl5ibcom	$⊢ y \in Grp \to ({Base}_{y} = x \to x \neq \emptyset)$
10	9	rexlimiv	$⊢ \exists y \in Grp {Base}_{y} = x \to x \neq \emptyset$
11	5 10	sylbi	$⊢ x \in Base [Grp] \to x \neq \emptyset$
12	11	adantl	$⊢ (dom card = V \land x \in Base [Grp]) \to x \neq \emptyset$
13		vex	$⊢ x \in V$
14	12 13	jctil	$⊢ (dom card = V \land x \in Base [Grp]) \to (x \in V \land x \neq \emptyset)$
15		ablgrp	$⊢ x \in Abel \to x \in Grp$
16	15	ssriv	$⊢ Abel \subseteq Grp$
17		imass2	$⊢ Abel \subseteq Grp \to Base [Abel] \subseteq Base [Grp]$
18	16 17	ax-mp	$⊢ Base [Abel] \subseteq Base [Grp]$
19		simprl	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to x \in V$
20		simpl	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to dom card = V$
21	19 20	eleqtrrd	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to x \in dom card$
22		simprr	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to x \neq \emptyset$
23		isnumbasgrplem3	$⊢ (x \in dom card \land x \neq \emptyset) \to x \in Base [Abel]$
24	21 22 23	syl2anc	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to x \in Base [Abel]$
25	18 24	sseldi	$⊢ (dom card = V \land (x \in V \land x \neq \emptyset)) \to x \in Base [Grp]$
26	14 25	impbida	$⊢ dom card = V \to (x \in Base [Grp] \leftrightarrow (x \in V \land x \neq \emptyset))$
27		eldifsn	$⊢ x \in (V ∖ \{\emptyset\}) \leftrightarrow (x \in V \land x \neq \emptyset)$
28	26 27	bitr4di	$⊢ dom card = V \to (x \in Base [Grp] \leftrightarrow x \in (V ∖ \{\emptyset\}))$
29	28	eqrdv	$⊢ dom card = V \to Base [Grp] = V ∖ \{\emptyset\}$
30		fvex	$⊢ har (x) \in V$
31	13 30	unex	$⊢ x \cup har (x) \in V$
32		ssun2	$⊢ har (x) \subseteq x \cup har (x)$
33		harn0	$⊢ x \in V \to har (x) \neq \emptyset$
34	13 33	ax-mp	$⊢ har (x) \neq \emptyset$
35		ssn0	$⊢ (har (x) \subseteq x \cup har (x) \land har (x) \neq \emptyset) \to x \cup har (x) \neq \emptyset$
36	32 34 35	mp2an	$⊢ x \cup har (x) \neq \emptyset$
37		eldifsn	$⊢ x \cup har (x) \in (V ∖ \{\emptyset\}) \leftrightarrow (x \cup har (x) \in V \land x \cup har (x) \neq \emptyset)$
38	31 36 37	mpbir2an	$⊢ x \cup har (x) \in (V ∖ \{\emptyset\})$
39	38	a1i	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to x \cup har (x) \in (V ∖ \{\emptyset\})$
40		id	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to Base [Grp] = V ∖ \{\emptyset\}$
41	39 40	eleqtrrd	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to x \cup har (x) \in Base [Grp]$
42		isnumbasgrp	$⊢ x \in dom card \leftrightarrow x \cup har (x) \in Base [Grp]$
43	41 42	sylibr	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to x \in dom card$
44	13	a1i	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to x \in V$
45	43 44	2thd	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to (x \in dom card \leftrightarrow x \in V)$
46	45	eqrdv	$⊢ Base [Grp] = V ∖ \{\emptyset\} \to dom card = V$
47	29 46	impbii	$⊢ dom card = V \leftrightarrow Base [Grp] = V ∖ \{\emptyset\}$
48	1 47	bitri	$⊢ CHOICE \leftrightarrow Base [Grp] = V ∖ \{\emptyset\}$

Metamath Proof Explorer

Theorem dfacbasgrp

Proof