Metamath Proof Explorer

Theorem efgi2

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

Ref Expression
Hypotheses efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
Assertion efgi2 ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → A ∼ ˙ B

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 fveq2 ⊢ a = A → T ⁡ a = T ⁡ A
6 5 rneqd ⊢ a = A → ran ⁡ T ⁡ a = ran ⁡ T ⁡ A
7 eceq1 ⊢ a = A → a r = A r
8 6 7 sseq12d ⊢ a = A → ran ⁡ T ⁡ a ⊆ a r ↔ ran ⁡ T ⁡ A ⊆ A r
9 8 rspcv ⊢ A ∈ W → ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → ran ⁡ T ⁡ A ⊆ A r
10 9 adantr ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → ran ⁡ T ⁡ A ⊆ A r
11 ssel ⊢ ran ⁡ T ⁡ A ⊆ A r → B ∈ ran ⁡ T ⁡ A → B ∈ A r
12 11 com12 ⊢ B ∈ ran ⁡ T ⁡ A → ran ⁡ T ⁡ A ⊆ A r → B ∈ A r
13 simpl ⊢ B ∈ A r ∧ A ∈ W → B ∈ A r
14 elecg ⊢ B ∈ A r ∧ A ∈ W → B ∈ A r ↔ A r B
15 13 14 mpbid ⊢ B ∈ A r ∧ A ∈ W → A r B
16 df-br ⊢ A r B ↔ A B ∈ r
17 15 16 sylib ⊢ B ∈ A r ∧ A ∈ W → A B ∈ r
18 17 expcom ⊢ A ∈ W → B ∈ A r → A B ∈ r
19 12 18 sylan9r ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → ran ⁡ T ⁡ A ⊆ A r → A B ∈ r
20 10 19 syld ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → A B ∈ r
21 20 adantld ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → A B ∈ r
22 21 alrimiv ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → ∀ r r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → A B ∈ r
23 opex ⊢ A B ∈ V
24 23 elintab ⊢ A B ∈ ⋂ r | r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r ↔ ∀ r r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r → A B ∈ r
25 22 24 sylibr ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → A B ∈ ⋂ r | r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r
26 1 2 3 4 efgval2 ⊢ ∼ ˙ = ⋂ r | r Er W ∧ ∀ a ∈ W ran ⁡ T ⁡ a ⊆ a r
27 25 26 eleqtrrdi ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → A B ∈ ∼ ˙
28 df-br ⊢ A ∼ ˙ B ↔ A B ∈ ∼ ˙
29 27 28 sylibr ⊢ A ∈ W ∧ B ∈ ran ⁡ T ⁡ A → A ∼ ˙ B