Metamath Proof Explorer


Theorem frmdup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses frmdup3.m M = freeMnd I
frmdup3.b B = Base G
frmdup3.u U = var FMnd I
Assertion frmdup3 G Mnd I V A : I B ∃! m M MndHom G m U = A

Proof

Step Hyp Ref Expression
1 frmdup3.m M = freeMnd I
2 frmdup3.b B = Base G
3 frmdup3.u U = var FMnd I
4 eqid x Word I G A x = x Word I G A x
5 simp1 G Mnd I V A : I B G Mnd
6 simp2 G Mnd I V A : I B I V
7 simp3 G Mnd I V A : I B A : I B
8 1 2 4 5 6 7 frmdup1 G Mnd I V A : I B x Word I G A x M MndHom G
9 5 adantr G Mnd I V A : I B y I G Mnd
10 6 adantr G Mnd I V A : I B y I I V
11 7 adantr G Mnd I V A : I B y I A : I B
12 simpr G Mnd I V A : I B y I y I
13 1 2 4 9 10 11 3 12 frmdup2 G Mnd I V A : I B y I x Word I G A x U y = A y
14 13 mpteq2dva G Mnd I V A : I B y I x Word I G A x U y = y I A y
15 eqid Base M = Base M
16 15 2 mhmf x Word I G A x M MndHom G x Word I G A x : Base M B
17 8 16 syl G Mnd I V A : I B x Word I G A x : Base M B
18 3 vrmdf I V U : I Word I
19 18 3ad2ant2 G Mnd I V A : I B U : I Word I
20 1 15 frmdbas I V Base M = Word I
21 20 3ad2ant2 G Mnd I V A : I B Base M = Word I
22 21 feq3d G Mnd I V A : I B U : I Base M U : I Word I
23 19 22 mpbird G Mnd I V A : I B U : I Base M
24 fcompt x Word I G A x : Base M B U : I Base M x Word I G A x U = y I x Word I G A x U y
25 17 23 24 syl2anc G Mnd I V A : I B x Word I G A x U = y I x Word I G A x U y
26 7 feqmptd G Mnd I V A : I B A = y I A y
27 14 25 26 3eqtr4d G Mnd I V A : I B x Word I G A x U = A
28 1 2 3 frmdup3lem G Mnd I V A : I B m M MndHom G m U = A m = x Word I G A x
29 28 expr G Mnd I V A : I B m M MndHom G m U = A m = x Word I G A x
30 29 ralrimiva G Mnd I V A : I B m M MndHom G m U = A m = x Word I G A x
31 coeq1 m = x Word I G A x m U = x Word I G A x U
32 31 eqeq1d m = x Word I G A x m U = A x Word I G A x U = A
33 32 eqreu x Word I G A x M MndHom G x Word I G A x U = A m M MndHom G m U = A m = x Word I G A x ∃! m M MndHom G m U = A
34 8 27 30 33 syl3anc G Mnd I V A : I B ∃! m M MndHom G m U = A