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⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
Assertion efgsdm ⊢F∈dom⁡S↔F∈WordW∖∅∧F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1

Proof

Step Hyp Ref Expression
1 efgval.w ⊢W=I⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡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..^ff⁡i∈ran⁡T⁡f⁡i−1↔∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1
17 8 16 anbi12d ⊢f=F→f⁡0∈D∧∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1↔F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1
18 1 2 3 4 5 6 efgsf ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
19 18 fdmi ⊢dom⁡S=t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡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..^tt⁡k∈ran⁡T⁡t⁡k−1↔∀i∈1..^tt⁡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..^tt⁡i∈ran⁡T⁡t⁡i−1↔∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1
36 27 35 bitrid ⊢t=f→∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1↔∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1
37 21 36 anbi12d ⊢t=f→t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1↔f⁡0∈D∧∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1
38 37 cbvrabv ⊢t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1=f∈WordW∖∅|f⁡0∈D∧∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1
39 19 38 eqtri ⊢dom⁡S=f∈WordW∖∅|f⁡0∈D∧∀i∈1..^ff⁡i∈ran⁡T⁡f⁡i−1
40 17 39 elrab2 ⊢F∈dom⁡S↔F∈WordW∖∅∧F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1
41 3anass ⊢F∈WordW∖∅∧F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1↔F∈WordW∖∅∧F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1
42 40 41 bitr4i ⊢F∈dom⁡S↔F∈WordW∖∅∧F⁡0∈D∧∀i∈1..^FF⁡i∈ran⁡T⁡F⁡i−1