Theorem efgi2

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
Assertion	efgi2	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → 𝐴 ∼ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2		efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5		fveq2	⊢ ( 𝑎 = 𝐴 → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝐴 ) )
6	5	rneqd	⊢ ( 𝑎 = 𝐴 → ran ( 𝑇 ‘ 𝑎 ) = ran ( 𝑇 ‘ 𝐴 ) )
7		eceq1	⊢ ( 𝑎 = 𝐴 → [ 𝑎 ] 𝑟 = [ 𝐴 ] 𝑟 )
8	6 7	sseq12d	⊢ ( 𝑎 = 𝐴 → ( ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ↔ ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 ) )
9	8	rspcv	⊢ ( 𝐴 ∈ 𝑊 → ( ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 → ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 → ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 ) )
11		ssel	⊢ ( ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 → ( 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) → 𝐵 ∈ [ 𝐴 ] 𝑟 ) )
12	11	com12	⊢ ( 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) → ( ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 → 𝐵 ∈ [ 𝐴 ] 𝑟 ) )
13		simpl	⊢ ( ( 𝐵 ∈ [ 𝐴 ] 𝑟 ∧ 𝐴 ∈ 𝑊 ) → 𝐵 ∈ [ 𝐴 ] 𝑟 )
14		elecg	⊢ ( ( 𝐵 ∈ [ 𝐴 ] 𝑟 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐵 ∈ [ 𝐴 ] 𝑟 ↔ 𝐴 𝑟 𝐵 ) )
15	13 14	mpbid	⊢ ( ( 𝐵 ∈ [ 𝐴 ] 𝑟 ∧ 𝐴 ∈ 𝑊 ) → 𝐴 𝑟 𝐵 )
16		df-br	⊢ ( 𝐴 𝑟 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 )
17	15 16	sylib	⊢ ( ( 𝐵 ∈ [ 𝐴 ] 𝑟 ∧ 𝐴 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 )
18	17	expcom	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐵 ∈ [ 𝐴 ] 𝑟 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
19	12 18	sylan9r	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ( ran ( 𝑇 ‘ 𝐴 ) ⊆ [ 𝐴 ] 𝑟 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
20	10 19	syld	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
21	20	adantld	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
22	21	alrimiv	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
23		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
24	23	elintab	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } ↔ ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑟 ) )
25	22 24	sylibr	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } )
26	1 2 3 4	efgval2	⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) }
27	25 26	eleqtrrdi	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ∼ )
28		df-br	⊢ ( 𝐴 ∼ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∼ )
29	27 28	sylibr	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran ( 𝑇 ‘ 𝐴 ) ) → 𝐴 ∼ 𝐵 )