Theorem frgpeccl

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

	Ref	Expression
Hypotheses	frgp0.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgp0.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	frgpeccl.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	frgpeccl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	frgpeccl	⊢ ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frgp0.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2		frgp0.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
3		frgpeccl.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
4		frgpeccl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
5	2	fvexi	⊢ ∼ ∈ V
6	5	ecelqsi	⊢ ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ ( 𝑊 / ∼ ) )
7	3	efgrcl	⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
8	7	simpld	⊢ ( 𝑋 ∈ 𝑊 → 𝐼 ∈ V )
9		eqid	⊢ ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
10	1 9 2	frgpval	⊢ ( 𝐼 ∈ V → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
11	8 10	syl	⊢ ( 𝑋 ∈ 𝑊 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ∼ ) )
12	7	simprd	⊢ ( 𝑋 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
13		2on	⊢ 2o ∈ On
14		xpexg	⊢ ( ( 𝐼 ∈ V ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
15	8 13 14	sylancl	⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 × 2o ) ∈ V )
16		eqid	⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
17	9 16	frmdbas	⊢ ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
18	15 17	syl	⊢ ( 𝑋 ∈ 𝑊 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
19	12 18	eqtr4d	⊢ ( 𝑋 ∈ 𝑊 → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
20	5	a1i	⊢ ( 𝑋 ∈ 𝑊 → ∼ ∈ V )
21		fvexd	⊢ ( 𝑋 ∈ 𝑊 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
22	11 19 20 21	qusbas	⊢ ( 𝑋 ∈ 𝑊 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐺 ) )
23	22 4	eqtr4di	⊢ ( 𝑋 ∈ 𝑊 → ( 𝑊 / ∼ ) = 𝐵 )
24	6 23	eleqtrd	⊢ ( 𝑋 ∈ 𝑊 → [ 𝑋 ] ∼ ∈ 𝐵 )