Theorem frmdbas

Description: The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
	frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
Assertion	frmdbas	$$⊢I\in V\to B=\mathrm{Word}I$$

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
2		frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
3		eqidd	$$⊢I\in V\to \mathrm{Word}I=\mathrm{Word}I$$
4		eqid	$$⊢{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}={\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}$$
5	1 3 4	frmdval	$$⊢I\in V\to M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}I⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}⟩\right\}$$
6	5	fveq2d	$$⊢I\in V\to {\mathrm{Base}}_M={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}I⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}⟩\right\}}$$
7		wrdexg	$$⊢I\in V\to \mathrm{Word}I\in \mathrm{V}$$
8		eqid	$$⊢\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}},\mathrm{Word}I⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}⟩\right\}$$
9	8	grpbase	$$⊢\mathrm{Word}I\in \mathrm{V}\to \mathrm{Word}I={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}I⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}⟩\right\}}$$
10	7 9	syl	$$⊢I\in V\to \mathrm{Word}I={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{Word}I⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(\mathrm{Word}I\times \mathrm{Word}I\right)}⟩\right\}}$$
11	6 10	eqtr4d	$$⊢I\in V\to {\mathrm{Base}}_M=\mathrm{Word}I$$
12	2 11	eqtrid	$$⊢I\in V\to B=\mathrm{Word}I$$