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 1 𝑜

Proof

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