This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
Assertion efgi0 ⊢ A ∈ W ∧ N ∈ 0 … A ∧ J ∈ I → A ∼ ˙ A splice N N ⟨“ J ∅ J 1 𝑜 ”⟩

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 0ex ⊢ ∅ ∈ V
4 3 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
5 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
6 4 5 eleqtrri ⊢ ∅ ∈ 2 𝑜
7 1 2 efgi ⊢ A ∈ W ∧ N ∈ 0 … A ∧ J ∈ I ∧ ∅ ∈ 2 𝑜 → A ∼ ˙ A splice N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩
8 6 7 mpanr2 ⊢ A ∈ W ∧ N ∈ 0 … A ∧ J ∈ I → A ∼ ˙ A splice N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩
9 8 3impa ⊢ A ∈ W ∧ N ∈ 0 … A ∧ J ∈ I → A ∼ ˙ A splice N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩
10 tru ⊢ ⊤
11 eqidd ⊢ ⊤ → J ∅ = J ∅
12 dif0 ⊢ 1 𝑜 ∖ ∅ = 1 𝑜
13 12 opeq2i ⊢ J 1 𝑜 ∖ ∅ = J 1 𝑜
14 13 a1i ⊢ ⊤ → J 1 𝑜 ∖ ∅ = J 1 𝑜
15 11 14 s2eqd ⊢ ⊤ → ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩ = ⟨“ J ∅ J 1 𝑜 ”⟩
16 oteq3 ⊢ ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩ = ⟨“ J ∅ J 1 𝑜 ”⟩ → N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩ = N N ⟨“ J ∅ J 1 𝑜 ”⟩
17 10 15 16 mp2b ⊢ N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩ = N N ⟨“ J ∅ J 1 𝑜 ”⟩
18 17 oveq2i ⊢ A splice N N ⟨“ J ∅ J 1 𝑜 ∖ ∅ ”⟩ = A splice N N ⟨“ J ∅ J 1 𝑜 ”⟩
19 9 18 breqtrdi ⊢ A ∈ W ∧ N ∈ 0 … A ∧ J ∈ I → A ∼ ˙ A splice N N ⟨“ J ∅ J 1 𝑜 ”⟩