Metamath Proof Explorer

Theorem efgsdm

Description: Elementhood in the domain of S , the set of sequences of extensions starting at an irreducible word. (Contributed by Mario Carneiro, 27-Sep-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 ”⟩
efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
Assertion efgsdm ⊢ F ∈ dom ⁡ S ↔ F ∈ Word W ∖ ∅ ∧ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1

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 efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
6 efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
7 fveq1 ⊢ f = F → f ⁡ 0 = F ⁡ 0
8 7 eleq1d ⊢ f = F → f ⁡ 0 ∈ D ↔ F ⁡ 0 ∈ D
9 fveq2 ⊢ f = F → f = F
10 9 oveq2d ⊢ f = F → 1 ..^ f = 1 ..^ F
11 fveq1 ⊢ f = F → f ⁡ i = F ⁡ i
12 fveq1 ⊢ f = F → f ⁡ i − 1 = F ⁡ i − 1
13 12 fveq2d ⊢ f = F → T ⁡ f ⁡ i − 1 = T ⁡ F ⁡ i − 1
14 13 rneqd ⊢ f = F → ran ⁡ T ⁡ f ⁡ i − 1 = ran ⁡ T ⁡ F ⁡ i − 1
15 11 14 eleq12d ⊢ f = F → f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1 ↔ F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1
16 10 15 raleqbidv ⊢ f = F → ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1 ↔ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1
17 8 16 anbi12d ⊢ f = F → f ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1 ↔ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1
18 1 2 3 4 5 6 efgsf ⊢ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W
19 18 fdmi ⊢ dom ⁡ S = t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1
20 fveq1 ⊢ t = f → t ⁡ 0 = f ⁡ 0
21 20 eleq1d ⊢ t = f → t ⁡ 0 ∈ D ↔ f ⁡ 0 ∈ D
22 fveq2 ⊢ k = i → t ⁡ k = t ⁡ i
23 fvoveq1 ⊢ k = i → t ⁡ k − 1 = t ⁡ i − 1
24 23 fveq2d ⊢ k = i → T ⁡ t ⁡ k − 1 = T ⁡ t ⁡ i − 1
25 24 rneqd ⊢ k = i → ran ⁡ T ⁡ t ⁡ k − 1 = ran ⁡ T ⁡ t ⁡ i − 1
26 22 25 eleq12d ⊢ k = i → t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ↔ t ⁡ i ∈ ran ⁡ T ⁡ t ⁡ i − 1
27 26 cbvralvw ⊢ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ↔ ∀ i ∈ 1 ..^ t t ⁡ i ∈ ran ⁡ T ⁡ t ⁡ i − 1
28 fveq2 ⊢ t = f → t = f
29 28 oveq2d ⊢ t = f → 1 ..^ t = 1 ..^ f
30 fveq1 ⊢ t = f → t ⁡ i = f ⁡ i
31 fveq1 ⊢ t = f → t ⁡ i − 1 = f ⁡ i − 1
32 31 fveq2d ⊢ t = f → T ⁡ t ⁡ i − 1 = T ⁡ f ⁡ i − 1
33 32 rneqd ⊢ t = f → ran ⁡ T ⁡ t ⁡ i − 1 = ran ⁡ T ⁡ f ⁡ i − 1
34 30 33 eleq12d ⊢ t = f → t ⁡ i ∈ ran ⁡ T ⁡ t ⁡ i − 1 ↔ f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
35 29 34 raleqbidv ⊢ t = f → ∀ i ∈ 1 ..^ t t ⁡ i ∈ ran ⁡ T ⁡ t ⁡ i − 1 ↔ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
36 27 35 syl5bb ⊢ t = f → ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ↔ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
37 21 36 anbi12d ⊢ t = f → t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ↔ f ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
38 37 cbvrabv ⊢ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 = f ∈ Word W ∖ ∅ | f ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
39 19 38 eqtri ⊢ dom ⁡ S = f ∈ Word W ∖ ∅ | f ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ f f ⁡ i ∈ ran ⁡ T ⁡ f ⁡ i − 1
40 17 39 elrab2 ⊢ F ∈ dom ⁡ S ↔ F ∈ Word W ∖ ∅ ∧ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1
41 3anass ⊢ F ∈ Word W ∖ ∅ ∧ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1 ↔ F ∈ Word W ∖ ∅ ∧ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1
42 40 41 bitr4i ⊢ F ∈ dom ⁡ S ↔ F ∈ Word W ∖ ∅ ∧ F ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ F F ⁡ i ∈ ran ⁡ T ⁡ F ⁡ i − 1