Theorem 0frgp

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

	Ref	Expression
Hypotheses	0frgp.g	⊢ 𝐺 = ( freeGrp ‘ ∅ )
	0frgp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	0frgp	⊢ 𝐵 ≈ 1o

Proof

Step	Hyp	Ref	Expression
1		0frgp.g	⊢ 𝐺 = ( freeGrp ‘ ∅ )
2		0frgp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		0ex	⊢ ∅ ∈ V
4	1	frgpgrp	⊢ ( ∅ ∈ V → 𝐺 ∈ Grp )
5	3 4	ax-mp	⊢ 𝐺 ∈ Grp
6		f0	⊢ ∅ : ∅ ⟶ 𝐵
7		eqid	⊢ ( ~FG ‘ ∅ ) = ( ~FG ‘ ∅ )
8		eqid	⊢ ( varFGrp ‘ ∅ ) = ( varFGrp ‘ ∅ )
9	7 8 1 2	vrgpf	⊢ ( ∅ ∈ V → ( varFGrp ‘ ∅ ) : ∅ ⟶ 𝐵 )
10		ffn	⊢ ( ( varFGrp ‘ ∅ ) : ∅ ⟶ 𝐵 → ( 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	⊢ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ∧ ∅ : ∅ ⟶ 𝐵 ) → ∃! 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅ )
16	5 3 6 15	mp3an	⊢ ∃! 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅
17		reurmo	⊢ ( ∃! 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅ → ∃* 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅ )
18	16 17	ax-mp	⊢ ∃* 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅
19	2	idghm	⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) )
20	5 19	ax-mp	⊢ ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 )
21		tru	⊢ ⊤
22	20 21	pm3.2i	⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ⊤ )
23		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
24	23 2	0ghm	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ Grp ) → ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) ∈ ( 𝐺 GrpHom 𝐺 ) )
25	5 5 24	mp2an	⊢ ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) ∈ ( 𝐺 GrpHom 𝐺 )
26	25 21	pm3.2i	⊢ ( ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ⊤ )
27		co02	⊢ ( 𝑓 ∘ ∅ ) = ∅
28	27	bitru	⊢ ( ( 𝑓 ∘ ∅ ) = ∅ ↔ ⊤ )
29	28	a1i	⊢ ( 𝑓 = ( I ↾ 𝐵 ) → ( ( 𝑓 ∘ ∅ ) = ∅ ↔ ⊤ ) )
30	28	a1i	⊢ ( 𝑓 = ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) → ( ( 𝑓 ∘ ∅ ) = ∅ ↔ ⊤ ) )
31	29 30	rmoi	⊢ ( ( ∃* 𝑓 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑓 ∘ ∅ ) = ∅ ∧ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ⊤ ) ∧ ( ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ⊤ ) ) → ( I ↾ 𝐵 ) = ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) )
32	18 22 26 31	mp3an	⊢ ( I ↾ 𝐵 ) = ( 𝐵 × { ( 0g ‘ 𝐺 ) } )
33		mptresid	⊢ ( I ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝑥 )
34		fconstmpt	⊢ ( 𝐵 × { ( 0g ‘ 𝐺 ) } ) = ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) )
35	32 33 34	3eqtr3i	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) )
36		mpteqb	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) ) ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 0g ‘ 𝐺 ) ) )
37		id	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐵 )
38	36 37	mprg	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) ) ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 0g ‘ 𝐺 ) )
39	35 38	mpbi	⊢ ∀ 𝑥 ∈ 𝐵 𝑥 = ( 0g ‘ 𝐺 )
40	39	rspec	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 = ( 0g ‘ 𝐺 ) )
41		velsn	⊢ ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ↔ 𝑥 = ( 0g ‘ 𝐺 ) )
42	40 41	sylibr	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ { ( 0g ‘ 𝐺 ) } )
43	42	ssriv	⊢ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) }
44	2 23	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
45	5 44	ax-mp	⊢ ( 0g ‘ 𝐺 ) ∈ 𝐵
46		snssi	⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝐵 → { ( 0g ‘ 𝐺 ) } ⊆ 𝐵 )
47	45 46	ax-mp	⊢ { ( 0g ‘ 𝐺 ) } ⊆ 𝐵
48	43 47	eqssi	⊢ 𝐵 = { ( 0g ‘ 𝐺 ) }
49		fvex	⊢ ( 0g ‘ 𝐺 ) ∈ V
50	49	ensn1	⊢ { ( 0g ‘ 𝐺 ) } ≈ 1o
51	48 50	eqbrtri	⊢ 𝐵 ≈ 1o