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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfac10 | |
|
2 | basfn | |
|
3 | ssv | |
|
4 | fvelimab | |
|
5 | 2 3 4 | mp2an | |
6 | eqid | |
|
7 | 6 | grpbn0 | |
8 | neeq1 | |
|
9 | 7 8 | syl5ibcom | |
10 | 9 | rexlimiv | |
11 | 5 10 | sylbi | |
12 | 11 | adantl | |
13 | vex | |
|
14 | 12 13 | jctil | |
15 | ablgrp | |
|
16 | 15 | ssriv | |
17 | imass2 | |
|
18 | 16 17 | ax-mp | |
19 | simprl | |
|
20 | simpl | |
|
21 | 19 20 | eleqtrrd | |
22 | simprr | |
|
23 | isnumbasgrplem3 | |
|
24 | 21 22 23 | syl2anc | |
25 | 18 24 | sselid | |
26 | 14 25 | impbida | |
27 | eldifsn | |
|
28 | 26 27 | bitr4di | |
29 | 28 | eqrdv | |
30 | fvex | |
|
31 | 13 30 | unex | |
32 | ssun2 | |
|
33 | harn0 | |
|
34 | 13 33 | ax-mp | |
35 | ssn0 | |
|
36 | 32 34 35 | mp2an | |
37 | eldifsn | |
|
38 | 31 36 37 | mpbir2an | |
39 | 38 | a1i | |
40 | id | |
|
41 | 39 40 | eleqtrrd | |
42 | isnumbasgrp | |
|
43 | 41 42 | sylibr | |
44 | 13 | a1i | |
45 | 43 44 | 2thd | |
46 | 45 | eqrdv | |
47 | 29 46 | impbii | |
48 | 1 47 | bitri | |