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

Metamath Proof Explorer

Theorem 0frgp

Proof