This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 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