Metamath Proof Explorer


Theorem efgi0

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses efgval.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r = ( ~FG𝐼 )
Assertion efgi0 ( ( 𝐴𝑊𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽𝐼 ) → 𝐴 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ ⟩ ) )

Proof

Step Hyp Ref Expression
1 efgval.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r = ( ~FG𝐼 )
3 0ex ∅ ∈ V
4 3 prid1 ∅ ∈ { ∅ , 1o }
5 df2o3 2o = { ∅ , 1o }
6 4 5 eleqtrri ∅ ∈ 2o
7 1 2 efgi ( ( ( 𝐴𝑊𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽𝐼 ∧ ∅ ∈ 2o ) ) → 𝐴 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ ) )
8 6 7 mpanr2 ( ( ( 𝐴𝑊𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝐽𝐼 ) → 𝐴 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ ) )
9 8 3impa ( ( 𝐴𝑊𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽𝐼 ) → 𝐴 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ ) )
10 tru
11 eqidd ( ⊤ → ⟨ 𝐽 , ∅ ⟩ = ⟨ 𝐽 , ∅ ⟩ )
12 dif0 ( 1o ∖ ∅ ) = 1o
13 12 opeq2i 𝐽 , ( 1o ∖ ∅ ) ⟩ = ⟨ 𝐽 , 1o
14 13 a1i ( ⊤ → ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ = ⟨ 𝐽 , 1o ⟩ )
15 11 14 s2eqd ( ⊤ → ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ )
16 oteq3 ( ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ → ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ ⟩ )
17 10 15 16 mp2b 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ ⟩
18 17 oveq2i ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , ( 1o ∖ ∅ ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ ⟩ )
19 9 18 breqtrdi ( ( 𝐴𝑊𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽𝐼 ) → 𝐴 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , ∅ ⟩ ⟨ 𝐽 , 1o ⟩ ”⟩ ⟩ ) )