Theorem vrgpf

Description: The mapping from the index set to the generators is a function into the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
	vrgpf.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	vrgpf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	vrgpf	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
2		vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
3		vrgpf.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
4		vrgpf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
5	1 2	vrgpfval	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
6		0ex	⊢ ∅ ∈ V
7	6	prid1	⊢ ∅ ∈ { ∅ , 1o }
8		df2o3	⊢ 2o = { ∅ , 1o }
9	7 8	eleqtrri	⊢ ∅ ∈ 2o
10		opelxpi	⊢ ( ( 𝑗 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
11	9 10	mpan2	⊢ ( 𝑗 ∈ 𝐼 → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
12	11	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ⟨ 𝑗 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
13	12	s1cld	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
14		2on	⊢ 2o ∈ On
15		xpexg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
16	14 15	mpan2	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × 2o ) ∈ V )
17	16	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ( 𝐼 × 2o ) ∈ V )
18		wrdexg	⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
19		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
20	17 18 19	3syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
21	13 20	eleqtrrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
22		eqid	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
23	3 1 22 4	frgpeccl	⊢ ( ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ∈ 𝑋 )
24	21 23	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐼 ) → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ∈ 𝑋 )
25	5 24	fmpt3d	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ 𝑋 )