Metamath Proof Explorer


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 CHOICEBaseGrp=V

Proof

Step Hyp Ref Expression
1 dfac10 CHOICEdomcard=V
2 basfn BaseFnV
3 ssv GrpV
4 fvelimab BaseFnVGrpVxBaseGrpyGrpBasey=x
5 2 3 4 mp2an xBaseGrpyGrpBasey=x
6 eqid Basey=Basey
7 6 grpbn0 yGrpBasey
8 neeq1 Basey=xBaseyx
9 7 8 syl5ibcom yGrpBasey=xx
10 9 rexlimiv yGrpBasey=xx
11 5 10 sylbi xBaseGrpx
12 11 adantl domcard=VxBaseGrpx
13 vex xV
14 12 13 jctil domcard=VxBaseGrpxVx
15 ablgrp xAbelxGrp
16 15 ssriv AbelGrp
17 imass2 AbelGrpBaseAbelBaseGrp
18 16 17 ax-mp BaseAbelBaseGrp
19 simprl domcard=VxVxxV
20 simpl domcard=VxVxdomcard=V
21 19 20 eleqtrrd domcard=VxVxxdomcard
22 simprr domcard=VxVxx
23 isnumbasgrplem3 xdomcardxxBaseAbel
24 21 22 23 syl2anc domcard=VxVxxBaseAbel
25 18 24 sselid domcard=VxVxxBaseGrp
26 14 25 impbida domcard=VxBaseGrpxVx
27 eldifsn xVxVx
28 26 27 bitr4di domcard=VxBaseGrpxV
29 28 eqrdv domcard=VBaseGrp=V
30 fvex harxV
31 13 30 unex xharxV
32 ssun2 harxxharx
33 harn0 xVharx
34 13 33 ax-mp harx
35 ssn0 harxxharxharxxharx
36 32 34 35 mp2an xharx
37 eldifsn xharxVxharxVxharx
38 31 36 37 mpbir2an xharxV
39 38 a1i BaseGrp=VxharxV
40 id BaseGrp=VBaseGrp=V
41 39 40 eleqtrrd BaseGrp=VxharxBaseGrp
42 isnumbasgrp xdomcardxharxBaseGrp
43 41 42 sylibr BaseGrp=Vxdomcard
44 13 a1i BaseGrp=VxV
45 43 44 2thd BaseGrp=VxdomcardxV
46 45 eqrdv BaseGrp=Vdomcard=V
47 29 46 impbii domcard=VBaseGrp=V
48 1 47 bitri CHOICEBaseGrp=V