Metamath Proof Explorer

Theorem 0frgp

Description: The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses 0frgp.g 
|- G = ( freeGrp ` (/) )
0frgp.b 
|- B = ( Base ` G )
Assertion 0frgp 
|- B ~~ 1o

Proof

Step Hyp Ref Expression
1 0frgp.g 
 |-  G = ( freeGrp ` (/) )
2 0frgp.b 
 |-  B = ( Base ` G )
3 0ex 
 |-  (/) e. _V
4 1 frgpgrp 
 |-  ( (/) e. _V -> G e. Grp )
5 3 4 ax-mp 
 |-  G e. Grp
6 f0 
 |-  (/) : (/) --> B
7 eqid 
 |-  ( ~FG ` (/) ) = ( ~FG ` (/) )
8 eqid 
 |-  ( varFGrp ` (/) ) = ( varFGrp ` (/) )
9 7 8 1 2 vrgpf 
 |-  ( (/) e. _V -> ( varFGrp ` (/) ) : (/) --> B )
10 ffn 
 |-  ( ( varFGrp ` (/) ) : (/) --> B -> ( varFGrp ` (/) ) Fn (/) )
11 3 9 10 mp2b 
 |-  ( varFGrp ` (/) ) Fn (/)
12 fn0 
 |-  ( ( varFGrp ` (/) ) Fn (/) <-> ( varFGrp ` (/) ) = (/) )
13 11 12 mpbi 
 |-  ( varFGrp ` (/) ) = (/)
14 13 eqcomi 
 |-  (/) = ( varFGrp ` (/) )
15 1 2 14 frgpup3 
 |-  ( ( G e. Grp /\ (/) e. _V /\ (/) : (/) --> B ) -> E! f e. ( G GrpHom G ) ( f o. (/) ) = (/) )
16 5 3 6 15 mp3an 
 |-  E! f e. ( G GrpHom G ) ( f o. (/) ) = (/)
17 reurmo 
 |-  ( E! f e. ( G GrpHom G ) ( f o. (/) ) = (/) -> E* f e. ( G GrpHom G ) ( f o. (/) ) = (/) )
18 16 17 ax-mp 
 |-  E* f e. ( G GrpHom G ) ( f o. (/) ) = (/)
19 2 idghm 
 |-  ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )
20 5 19 ax-mp 
 |-  ( _I |` B ) e. ( G GrpHom G )
21 tru 
 |-  T.
22 20 21 pm3.2i 
 |-  ( ( _I |` B ) e. ( G GrpHom G ) /\ T. )
23 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
24 23 2 0ghm 
 |-  ( ( G e. Grp /\ G e. Grp ) -> ( B X. { ( 0g ` G ) } ) e. ( G GrpHom G ) )
25 5 5 24 mp2an 
 |-  ( B X. { ( 0g ` G ) } ) e. ( G GrpHom G )
26 25 21 pm3.2i 
 |-  ( ( B X. { ( 0g ` G ) } ) e. ( G GrpHom G ) /\ T. )
27 co02 
 |-  ( f o. (/) ) = (/)
28 27 bitru 
 |-  ( ( f o. (/) ) = (/) <-> T. )
29 28 a1i 
 |-  ( f = ( _I |` B ) -> ( ( f o. (/) ) = (/) <-> T. ) )
30 28 a1i 
 |-  ( f = ( B X. { ( 0g ` G ) } ) -> ( ( f o. (/) ) = (/) <-> T. ) )
31 29 30 rmoi 
 |-  ( ( E* f e. ( G GrpHom G ) ( f o. (/) ) = (/) /\ ( ( _I |` B ) e. ( G GrpHom G ) /\ T. ) /\ ( ( B X. { ( 0g ` G ) } ) e. ( G GrpHom G ) /\ T. ) ) -> ( _I |` B ) = ( B X. { ( 0g ` G ) } ) )
32 18 22 26 31 mp3an 
 |-  ( _I |` B ) = ( B X. { ( 0g ` G ) } )
33 mptresid 
 |-  ( _I |` B ) = ( x e. B |-> x )
34 fconstmpt 
 |-  ( B X. { ( 0g ` G ) } ) = ( x e. B |-> ( 0g ` G ) )
35 32 33 34 3eqtr3i 
 |-  ( x e. B |-> x ) = ( x e. B |-> ( 0g ` G ) )
36 mpteqb 
 |-  ( A. x e. B x e. B -> ( ( x e. B |-> x ) = ( x e. B |-> ( 0g ` G ) ) <-> A. x e. B x = ( 0g ` G ) ) )
37 id 
 |-  ( x e. B -> x e. B )
38 36 37 mprg 
 |-  ( ( x e. B |-> x ) = ( x e. B |-> ( 0g ` G ) ) <-> A. x e. B x = ( 0g ` G ) )
39 35 38 mpbi 
 |-  A. x e. B x = ( 0g ` G )
40 39 rspec 
 |-  ( x e. B -> x = ( 0g ` G ) )
41 velsn 
 |-  ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) )
42 40 41 sylibr 
 |-  ( x e. B -> x e. { ( 0g ` G ) } )
43 42 ssriv 
 |-  B C_ { ( 0g ` G ) }
44 2 23 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
45 5 44 ax-mp 
 |-  ( 0g ` G ) e. B
46 snssi 
 |-  ( ( 0g ` G ) e. B -> { ( 0g ` G ) } C_ B )
47 45 46 ax-mp 
 |-  { ( 0g ` G ) } C_ B
48 43 47 eqssi 
 |-  B = { ( 0g ` G ) }
49 fvex 
 |-  ( 0g ` G ) e. _V
50 49 ensn1 
 |-  { ( 0g ` G ) } ~~ 1o
51 48 50 eqbrtri 
 |-  B ~~ 1o