Theorem frgpeccl

Description: Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	frgp0.m	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
	frgp0.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
	frgpeccl.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
	frgpeccl.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	frgpeccl	$$⊢X\in W\to \left[X\right]\underset{\dot{}}{\sim }\in B$$

Proof

Step	Hyp	Ref	Expression
1		frgp0.m	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
2		frgp0.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
3		frgpeccl.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
4		frgpeccl.b	$$⊢B={\mathrm{Base}}_G$$
5	2	fvexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
6	5	ecelqsi	$$⊢X\in W\to \left[X\right]\underset{\dot{}}{\sim }\in \left(W/\underset{\dot{}}{\sim }\right)$$
7	3	efgrcl	$$⊢X\in W\to \left(I\in \mathrm{V}\wedge W=\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
8	7	simpld	$$⊢X\in W\to I\in \mathrm{V}$$
9		eqid	$$⊢\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
10	1 9 2	frgpval	$$⊢I\in \mathrm{V}\to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
11	8 10	syl	$$⊢X\in W\to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
12	7	simprd	$$⊢X\in W\to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
13		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
14		xpexg	$$⊢\left(I\in \mathrm{V}\wedge 2_{𝑜}\in \mathrm{On}\right)\to I\times 2_{𝑜}\in \mathrm{V}$$
15	8 13 14	sylancl	$$⊢X\in W\to I\times 2_{𝑜}\in \mathrm{V}$$
16		eqid	$$⊢{\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
17	9 16	frmdbas	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
18	15 17	syl	$$⊢X\in W\to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
19	12 18	eqtr4d	$$⊢X\in W\to W={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
20	5	a1i	$$⊢X\in W\to \underset{\dot{}}{\sim }\in \mathrm{V}$$
21		fvexd	$$⊢X\in W\to \mathrm{freeMnd}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
22	11 19 20 21	qusbas	$$⊢X\in W\to W/\underset{\dot{}}{\sim }={\mathrm{Base}}_G$$
23	22 4	eqtr4di	$$⊢X\in W\to W/\underset{\dot{}}{\sim }=B$$
24	6 23	eleqtrd	$$⊢X\in W\to \left[X\right]\underset{\dot{}}{\sim }\in B$$