Theorem frmdval

Description: Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Hypotheses	frmdval.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
	frmdval.b	$$⊢I\in V\to B=\mathrm{Word}I$$
	frmdval.p	$$⊢\underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
Assertion	frmdval	$$⊢I\in V\to M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		frmdval.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
2		frmdval.b	$$⊢I\in V\to B=\mathrm{Word}I$$
3		frmdval.p	$$⊢\underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
4		df-frmd	$$⊢\mathrm{freeMnd}=\left(i\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}\right)$$
5		wrdeq	$$⊢i=I\to \mathrm{Word}i=\mathrm{Word}I$$
6	2	eqcomd	$$⊢I\in V\to \mathrm{Word}I=B$$
7	5 6	sylan9eqr	$$⊢\left(I\in V\wedge i=I\right)\to \mathrm{Word}i=B$$
8	7	opeq2d	$$⊢\left(I\in V\wedge i=I\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
9	7	sqxpeqd	$$⊢\left(I\in V\wedge i=I\right)\to \mathrm{Word}i\times \mathrm{Word}i=B\times B$$
10	9	reseq2d	$$⊢\left(I\in V\wedge i=I\right)\to {\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
11	10 3	syl6eqr	$$⊢\left(I\in V\wedge i=I\right)\to {\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}=\underset{\dot{}}{+}$$
12	11	opeq2d	$$⊢\left(I\in V\wedge i=I\right)\to ⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩$$
13	8 12	preq12d	$$⊢\left(I\in V\wedge i=I\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}i⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}i\times \mathrm{Word}i\right)}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
14		elex	$$⊢I\in V\to I\in \mathrm{V}$$
15		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}\in \mathrm{V}$$
16	15	a1i	$$⊢I\in V\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}\in \mathrm{V}$$
17	4 13 14 16	fvmptd2	$$⊢I\in V\to \mathrm{freeMnd}\left(I\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
18	1 17	syl5eq	$$⊢I\in V\to M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$