Metamath Proof Explorer

Theorem efgsfo

Description: For any word, there is a sequence of extensions starting at a reduced word and ending at the target word, such that each word in the chain is an extension of the previous (inserting an element and its inverse at adjacent indices somewhere in the sequence). (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 efgsfo ⊢S:dom⁡S⟶ontoW

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 1 2 3 4 5 6 efgsf ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
8 7 fdmi ⊢dom⁡S=t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1
9 8 feq2i ⊢S:dom⁡S⟶W↔S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
10 7 9 mpbir ⊢S:dom⁡S⟶W
11 frn ⊢S:dom⁡S⟶W→ran⁡S⊆W
12 10 11 ax-mp ⊢ran⁡S⊆W
13 fviss ⊢I⁡WordI×2𝑜⊆WordI×2𝑜
14 1 13 eqsstri ⊢W⊆WordI×2𝑜
15 14 sseli ⊢c∈W→c∈WordI×2𝑜
16 lencl ⊢c∈WordI×2𝑜→c∈ℕ0
17 15 16 syl ⊢c∈W→c∈ℕ0
18 peano2nn0 ⊢c∈ℕ0→c+1∈ℕ0
19 14 sseli ⊢a∈W→a∈WordI×2𝑜
20 lencl ⊢a∈WordI×2𝑜→a∈ℕ0
21 19 20 syl ⊢a∈W→a∈ℕ0
22 nn0nlt0 ⊢a∈ℕ0→¬a<0
23 breq2 ⊢b=0→a<b↔a<0
24 23 notbid ⊢b=0→¬a<b↔¬a<0
25 22 24 imbitrrid ⊢b=0→a∈ℕ0→¬a<b
26 21 25 syl5 ⊢b=0→a∈W→¬a<b
27 26 ralrimiv ⊢b=0→∀a∈W¬a<b
28 rabeq0 ⊢a∈W|a<b=∅↔∀a∈W¬a<b
29 27 28 sylibr ⊢b=0→a∈W|a<b=∅
30 29 sseq1d ⊢b=0→a∈W|a<b⊆ran⁡S↔∅⊆ran⁡S
31 breq2 ⊢b=d→a<b↔a<d
32 31 rabbidv ⊢b=d→a∈W|a<b=a∈W|a<d
33 32 sseq1d ⊢b=d→a∈W|a<b⊆ran⁡S↔a∈W|a<d⊆ran⁡S
34 breq2 ⊢b=d+1→a<b↔a<d+1
35 34 rabbidv ⊢b=d+1→a∈W|a<b=a∈W|a<d+1
36 35 sseq1d ⊢b=d+1→a∈W|a<b⊆ran⁡S↔a∈W|a<d+1⊆ran⁡S
37 breq2 ⊢b=c+1→a<b↔a<c+1
38 37 rabbidv ⊢b=c+1→a∈W|a<b=a∈W|a<c+1
39 38 sseq1d ⊢b=c+1→a∈W|a<b⊆ran⁡S↔a∈W|a<c+1⊆ran⁡S
40 0ss ⊢∅⊆ran⁡S
41 simpr ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S→a∈W|a<d⊆ran⁡S
42 fveqeq2 ⊢a=c→a=d↔c=d
43 42 cbvrabv ⊢a∈W|a=d=c∈W|c=d
44 eliun ⊢c∈⋃x∈Wran⁡T⁡x↔∃x∈Wc∈ran⁡T⁡x
45 fveq2 ⊢x=b→T⁡x=T⁡b
46 45 rneqd ⊢x=b→ran⁡T⁡x=ran⁡T⁡b
47 46 eleq2d ⊢x=b→c∈ran⁡T⁡x↔c∈ran⁡T⁡b
48 47 cbvrexvw ⊢∃x∈Wc∈ran⁡T⁡x↔∃b∈Wc∈ran⁡T⁡b
49 44 48 bitri ⊢c∈⋃x∈Wran⁡T⁡x↔∃b∈Wc∈ran⁡T⁡b
50 simpl1r ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→a∈W|a<d⊆ran⁡S
51 fveq2 ⊢a=b→a=b
52 51 breq1d ⊢a=b→a<d↔b<d
53 simprl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈W
54 14 53 sselid ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈WordI×2𝑜
55 lencl ⊢b∈WordI×2𝑜→b∈ℕ0
56 54 55 syl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈ℕ0
57 56 nn0red ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈ℝ
58 2rp ⊢2∈ℝ+
59 ltaddrp ⊢b∈ℝ∧2∈ℝ+→b<b+2
60 57 58 59 sylancl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b<b+2
61 1 2 3 4 efgtlen ⊢b∈W∧c∈ran⁡T⁡b→c=b+2
62 61 adantl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→c=b+2
63 simpl3 ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→c=d
64 62 63 eqtr3d ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b+2=d
65 60 64 breqtrd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b<d
66 52 53 65 elrabd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈a∈W|a<d
67 50 66 sseldd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→b∈ran⁡S
68 ffn ⊢S:dom⁡S⟶W→SFndom⁡S
69 10 68 ax-mp ⊢SFndom⁡S
70 fvelrnb ⊢SFndom⁡S→b∈ran⁡S↔∃o∈dom⁡SS⁡o=b
71 69 70 ax-mp ⊢b∈ran⁡S↔∃o∈dom⁡SS⁡o=b
72 67 71 sylib ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→∃o∈dom⁡SS⁡o=b
73 simprrl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→o∈dom⁡S
74 1 2 3 4 5 6 efgsdm ⊢o∈dom⁡S↔o∈WordW∖∅∧o⁡0∈D∧∀i∈1..^oo⁡i∈ran⁡T⁡o⁡i−1
75 74 simp1bi ⊢o∈dom⁡S→o∈WordW∖∅
76 eldifi ⊢o∈WordW∖∅→o∈WordW
77 73 75 76 3syl ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→o∈WordW
78 simpl2 ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→c∈W
79 simprlr ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→c∈ran⁡T⁡b
80 simprrr ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→S⁡o=b
81 80 fveq2d ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→T⁡S⁡o=T⁡b
82 81 rneqd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→ran⁡T⁡S⁡o=ran⁡T⁡b
83 79 82 eleqtrrd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→c∈ran⁡T⁡S⁡o
84 1 2 3 4 5 6 efgsp1 ⊢o∈dom⁡S∧c∈ran⁡T⁡S⁡o→o++⟨“c”⟩∈dom⁡S
85 73 83 84 syl2anc ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→o++⟨“c”⟩∈dom⁡S
86 1 2 3 4 5 6 efgsval2 ⊢o∈WordW∧c∈W∧o++⟨“c”⟩∈dom⁡S→S⁡o++⟨“c”⟩=c
87 77 78 85 86 syl3anc ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→S⁡o++⟨“c”⟩=c
88 fnfvelrn ⊢SFndom⁡S∧o++⟨“c”⟩∈dom⁡S→S⁡o++⟨“c”⟩∈ran⁡S
89 69 85 88 sylancr ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→S⁡o++⟨“c”⟩∈ran⁡S
90 87 89 eqeltrrd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→c∈ran⁡S
91 90 anassrs ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b∧o∈dom⁡S∧S⁡o=b→c∈ran⁡S
92 72 91 rexlimddv ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d∧b∈W∧c∈ran⁡T⁡b→c∈ran⁡S
93 92 rexlimdvaa ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d→∃b∈Wc∈ran⁡T⁡b→c∈ran⁡S
94 49 93 biimtrid ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d→c∈⋃x∈Wran⁡T⁡x→c∈ran⁡S
95 eldif ⊢c∈W∖⋃x∈Wran⁡T⁡x↔c∈W∧¬c∈⋃x∈Wran⁡T⁡x
96 5 eleq2i ⊢c∈D↔c∈W∖⋃x∈Wran⁡T⁡x
97 1 2 3 4 5 6 efgs1 ⊢c∈D→⟨“c”⟩∈dom⁡S
98 96 97 sylbir ⊢c∈W∖⋃x∈Wran⁡T⁡x→⟨“c”⟩∈dom⁡S
99 95 98 sylbir ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→⟨“c”⟩∈dom⁡S
100 1 2 3 4 5 6 efgsval ⊢⟨“c”⟩∈dom⁡S→S⁡⟨“c”⟩=⟨“c”⟩⁡⟨“c”⟩−1
101 99 100 syl ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→S⁡⟨“c”⟩=⟨“c”⟩⁡⟨“c”⟩−1
102 s1len ⊢⟨“c”⟩=1
103 102 oveq1i ⊢⟨“c”⟩−1=1−1
104 1m1e0 ⊢1−1=0
105 103 104 eqtri ⊢⟨“c”⟩−1=0
106 105 fveq2i ⊢⟨“c”⟩⁡⟨“c”⟩−1=⟨“c”⟩⁡0
107 106 a1i ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→⟨“c”⟩⁡⟨“c”⟩−1=⟨“c”⟩⁡0
108 s1fv ⊢c∈W→⟨“c”⟩⁡0=c
109 108 adantr ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→⟨“c”⟩⁡0=c
110 101 107 109 3eqtrd ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→S⁡⟨“c”⟩=c
111 fnfvelrn ⊢SFndom⁡S∧⟨“c”⟩∈dom⁡S→S⁡⟨“c”⟩∈ran⁡S
112 69 99 111 sylancr ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→S⁡⟨“c”⟩∈ran⁡S
113 110 112 eqeltrrd ⊢c∈W∧¬c∈⋃x∈Wran⁡T⁡x→c∈ran⁡S
114 113 ex ⊢c∈W→¬c∈⋃x∈Wran⁡T⁡x→c∈ran⁡S
115 114 3ad2ant2 ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d→¬c∈⋃x∈Wran⁡T⁡x→c∈ran⁡S
116 94 115 pm2.61d ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S∧c∈W∧c=d→c∈ran⁡S
117 116 rabssdv ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S→c∈W|c=d⊆ran⁡S
118 43 117 eqsstrid ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S→a∈W|a=d⊆ran⁡S
119 41 118 unssd ⊢d∈ℕ0∧a∈W|a<d⊆ran⁡S→a∈W|a<d∪a∈W|a=d⊆ran⁡S
120 119 ex ⊢d∈ℕ0→a∈W|a<d⊆ran⁡S→a∈W|a<d∪a∈W|a=d⊆ran⁡S
121 id ⊢d∈ℕ0→d∈ℕ0
122 nn0leltp1 ⊢a∈ℕ0∧d∈ℕ0→a≤d↔a<d+1
123 21 121 122 syl2anr ⊢d∈ℕ0∧a∈W→a≤d↔a<d+1
124 21 nn0red ⊢a∈W→a∈ℝ
125 nn0re ⊢d∈ℕ0→d∈ℝ
126 leloe ⊢a∈ℝ∧d∈ℝ→a≤d↔a<d∨a=d
127 124 125 126 syl2anr ⊢d∈ℕ0∧a∈W→a≤d↔a<d∨a=d
128 123 127 bitr3d ⊢d∈ℕ0∧a∈W→a<d+1↔a<d∨a=d
129 128 rabbidva ⊢d∈ℕ0→a∈W|a<d+1=a∈W|a<d∨a=d
130 unrab ⊢a∈W|a<d∪a∈W|a=d=a∈W|a<d∨a=d
131 129 130 eqtr4di ⊢d∈ℕ0→a∈W|a<d+1=a∈W|a<d∪a∈W|a=d
132 131 sseq1d ⊢d∈ℕ0→a∈W|a<d+1⊆ran⁡S↔a∈W|a<d∪a∈W|a=d⊆ran⁡S
133 120 132 sylibrd ⊢d∈ℕ0→a∈W|a<d⊆ran⁡S→a∈W|a<d+1⊆ran⁡S
134 30 33 36 39 40 133 nn0ind ⊢c+1∈ℕ0→a∈W|a<c+1⊆ran⁡S
135 17 18 134 3syl ⊢c∈W→a∈W|a<c+1⊆ran⁡S
136 fveq2 ⊢a=c→a=c
137 136 breq1d ⊢a=c→a<c+1↔c<c+1
138 id ⊢c∈W→c∈W
139 17 nn0red ⊢c∈W→c∈ℝ
140 139 ltp1d ⊢c∈W→c<c+1
141 137 138 140 elrabd ⊢c∈W→c∈a∈W|a<c+1
142 135 141 sseldd ⊢c∈W→c∈ran⁡S
143 142 ssriv ⊢W⊆ran⁡S
144 12 143 eqssi ⊢ran⁡S=W
145 dffo2 ⊢S:dom⁡S⟶ontoW↔S:dom⁡S⟶W∧ran⁡S=W
146 10 144 145 mpbir2an ⊢S:dom⁡S⟶ontoW