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 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 x Base Grp y Grp Base y = x
5 2 3 4 mp2an x Base Grp y Grp Base y = x
6 eqid Base y = Base y
7 6 grpbn0 y Grp Base y
8 neeq1 Base y = x Base y x
9 7 8 syl5ibcom y Grp Base y = x x
10 9 rexlimiv y Grp Base y = x x
11 5 10 sylbi x Base Grp x
12 11 adantl dom card = V x Base Grp x
13 vex x V
14 12 13 jctil dom card = V x Base Grp x V x
15 ablgrp x Abel x 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 x V x x V
20 simpl dom card = V x V x dom card = V
21 19 20 eleqtrrd dom card = V x V x x dom card
22 simprr dom card = V x V x x
23 isnumbasgrplem3 x dom card x x Base Abel
24 21 22 23 syl2anc dom card = V x V x x Base Abel
25 18 24 sseldi dom card = V x V x x Base Grp
26 14 25 impbida dom card = V x Base Grp x V x
27 eldifsn x V x V x
28 26 27 bitr4di dom card = V x Base Grp x V
29 28 eqrdv dom card = V Base Grp = V
30 fvex har x V
31 13 30 unex x har x V
32 ssun2 har x x har x
33 harn0 x V har x
34 13 33 ax-mp har x
35 ssn0 har x x har x har x x har x
36 32 34 35 mp2an x har x
37 eldifsn x har x V x har x V x har x
38 31 36 37 mpbir2an x har x V
39 38 a1i Base Grp = V x har x V
40 id Base Grp = V Base Grp = V
41 39 40 eleqtrrd Base Grp = V x har x Base Grp
42 isnumbasgrp x dom card x har x Base Grp
43 41 42 sylibr Base Grp = V x dom card
44 13 a1i Base Grp = V x V
45 43 44 2thd Base Grp = V x dom card x 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