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 C_ _V
4 fvelimab 
 |-  ( ( Base Fn _V /\ Grp C_ _V ) -> ( x e. ( Base " Grp ) <-> E. y e. Grp ( Base ` y ) = x ) )
5 2 3 4 mp2an 
 |-  ( x e. ( Base " Grp ) <-> E. y e. Grp ( Base ` y ) = x )
6 eqid 
 |-  ( Base ` y ) = ( Base ` y )
7 6 grpbn0 
 |-  ( y e. Grp -> ( Base ` y ) =/= (/) )
8 neeq1 
 |-  ( ( Base ` y ) = x -> ( ( Base ` y ) =/= (/) <-> x =/= (/) ) )
9 7 8 syl5ibcom 
 |-  ( y e. Grp -> ( ( Base ` y ) = x -> x =/= (/) ) )
10 9 rexlimiv 
 |-  ( E. y e. Grp ( Base ` y ) = x -> x =/= (/) )
11 5 10 sylbi 
 |-  ( x e. ( Base " Grp ) -> x =/= (/) )
12 11 adantl 
 |-  ( ( dom card = _V /\ x e. ( Base " Grp ) ) -> x =/= (/) )
13 vex 
 |-  x e. _V
14 12 13 jctil 
 |-  ( ( dom card = _V /\ x e. ( Base " Grp ) ) -> ( x e. _V /\ x =/= (/) ) )
15 ablgrp 
 |-  ( x e. Abel -> x e. Grp )
16 15 ssriv 
 |-  Abel C_ Grp
17 imass2 
 |-  ( Abel C_ Grp -> ( Base " Abel ) C_ ( Base " Grp ) )
18 16 17 ax-mp 
 |-  ( Base " Abel ) C_ ( Base " Grp )
19 simprl 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> x e. _V )
20 simpl 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> dom card = _V )
21 19 20 eleqtrrd 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> x e. dom card )
22 simprr 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> x =/= (/) )
23 isnumbasgrplem3 
 |-  ( ( x e. dom card /\ x =/= (/) ) -> x e. ( Base " Abel ) )
24 21 22 23 syl2anc 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> x e. ( Base " Abel ) )
25 18 24 sselid 
 |-  ( ( dom card = _V /\ ( x e. _V /\ x =/= (/) ) ) -> x e. ( Base " Grp ) )
26 14 25 impbida 
 |-  ( dom card = _V -> ( x e. ( Base " Grp ) <-> ( x e. _V /\ x =/= (/) ) ) )
27 eldifsn 
 |-  ( x e. ( _V \ { (/) } ) <-> ( x e. _V /\ x =/= (/) ) )
28 26 27 bitr4di 
 |-  ( dom card = _V -> ( x e. ( Base " Grp ) <-> x e. ( _V \ { (/) } ) ) )
29 28 eqrdv 
 |-  ( dom card = _V -> ( Base " Grp ) = ( _V \ { (/) } ) )
30 fvex 
 |-  ( har ` x ) e. _V
31 13 30 unex 
 |-  ( x u. ( har ` x ) ) e. _V
32 ssun2 
 |-  ( har ` x ) C_ ( x u. ( har ` x ) )
33 harn0 
 |-  ( x e. _V -> ( har ` x ) =/= (/) )
34 13 33 ax-mp 
 |-  ( har ` x ) =/= (/)
35 ssn0 
 |-  ( ( ( har ` x ) C_ ( x u. ( har ` x ) ) /\ ( har ` x ) =/= (/) ) -> ( x u. ( har ` x ) ) =/= (/) )
36 32 34 35 mp2an 
 |-  ( x u. ( har ` x ) ) =/= (/)
37 eldifsn 
 |-  ( ( x u. ( har ` x ) ) e. ( _V \ { (/) } ) <-> ( ( x u. ( har ` x ) ) e. _V /\ ( x u. ( har ` x ) ) =/= (/) ) )
38 31 36 37 mpbir2an 
 |-  ( x u. ( har ` x ) ) e. ( _V \ { (/) } )
39 38 a1i 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> ( x u. ( har ` x ) ) e. ( _V \ { (/) } ) )
40 id 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> ( Base " Grp ) = ( _V \ { (/) } ) )
41 39 40 eleqtrrd 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> ( x u. ( har ` x ) ) e. ( Base " Grp ) )
42 isnumbasgrp 
 |-  ( x e. dom card <-> ( x u. ( har ` x ) ) e. ( Base " Grp ) )
43 41 42 sylibr 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> x e. dom card )
44 13 a1i 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> x e. _V )
45 43 44 2thd 
 |-  ( ( Base " Grp ) = ( _V \ { (/) } ) -> ( x e. dom card <-> x e. _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 \ { (/) } ) )