# 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}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
Assertion efgsfo ${⊢}{S}:\mathrm{dom}{S}\underset{onto}{⟶}{W}$

### Proof

Step Hyp Ref Expression
1 efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 efgval.r
3 efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
4 efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
5 efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
6 efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
7 1 2 3 4 5 6 efgsf ${⊢}{S}:\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟶{W}$
8 7 fdmi ${⊢}\mathrm{dom}{S}=\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}$
9 8 feq2i ${⊢}{S}:\mathrm{dom}{S}⟶{W}↔{S}:\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟶{W}$
10 7 9 mpbir ${⊢}{S}:\mathrm{dom}{S}⟶{W}$
11 frn ${⊢}{S}:\mathrm{dom}{S}⟶{W}\to \mathrm{ran}{S}\subseteq {W}$
12 10 11 ax-mp ${⊢}\mathrm{ran}{S}\subseteq {W}$
13 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
14 1 13 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
15 14 sseli ${⊢}{c}\in {W}\to {c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
16 lencl ${⊢}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{c}\right|\in {ℕ}_{0}$
17 15 16 syl ${⊢}{c}\in {W}\to \left|{c}\right|\in {ℕ}_{0}$
18 peano2nn0 ${⊢}\left|{c}\right|\in {ℕ}_{0}\to \left|{c}\right|+1\in {ℕ}_{0}$
19 14 sseli ${⊢}{a}\in {W}\to {a}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
20 lencl ${⊢}{a}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{a}\right|\in {ℕ}_{0}$
21 19 20 syl ${⊢}{a}\in {W}\to \left|{a}\right|\in {ℕ}_{0}$
22 nn0nlt0 ${⊢}\left|{a}\right|\in {ℕ}_{0}\to ¬\left|{a}\right|<0$
23 breq2 ${⊢}{b}=0\to \left(\left|{a}\right|<{b}↔\left|{a}\right|<0\right)$
24 23 notbid ${⊢}{b}=0\to \left(¬\left|{a}\right|<{b}↔¬\left|{a}\right|<0\right)$
25 22 24 syl5ibr ${⊢}{b}=0\to \left(\left|{a}\right|\in {ℕ}_{0}\to ¬\left|{a}\right|<{b}\right)$
26 21 25 syl5 ${⊢}{b}=0\to \left({a}\in {W}\to ¬\left|{a}\right|<{b}\right)$
27 26 ralrimiv ${⊢}{b}=0\to \forall {a}\in {W}\phantom{\rule{.4em}{0ex}}¬\left|{a}\right|<{b}$
28 rabeq0 ${⊢}\left\{{a}\in {W}|\left|{a}\right|<{b}\right\}=\varnothing ↔\forall {a}\in {W}\phantom{\rule{.4em}{0ex}}¬\left|{a}\right|<{b}$
29 27 28 sylibr ${⊢}{b}=0\to \left\{{a}\in {W}|\left|{a}\right|<{b}\right\}=\varnothing$
30 29 sseq1d ${⊢}{b}=0\to \left(\left\{{a}\in {W}|\left|{a}\right|<{b}\right\}\subseteq \mathrm{ran}{S}↔\varnothing \subseteq \mathrm{ran}{S}\right)$
31 breq2 ${⊢}{b}={d}\to \left(\left|{a}\right|<{b}↔\left|{a}\right|<{d}\right)$
32 31 rabbidv ${⊢}{b}={d}\to \left\{{a}\in {W}|\left|{a}\right|<{b}\right\}=\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}$
33 32 sseq1d ${⊢}{b}={d}\to \left(\left\{{a}\in {W}|\left|{a}\right|<{b}\right\}\subseteq \mathrm{ran}{S}↔\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)$
34 breq2 ${⊢}{b}={d}+1\to \left(\left|{a}\right|<{b}↔\left|{a}\right|<{d}+1\right)$
35 34 rabbidv ${⊢}{b}={d}+1\to \left\{{a}\in {W}|\left|{a}\right|<{b}\right\}=\left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}$
36 35 sseq1d ${⊢}{b}={d}+1\to \left(\left\{{a}\in {W}|\left|{a}\right|<{b}\right\}\subseteq \mathrm{ran}{S}↔\left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}\subseteq \mathrm{ran}{S}\right)$
37 breq2 ${⊢}{b}=\left|{c}\right|+1\to \left(\left|{a}\right|<{b}↔\left|{a}\right|<\left|{c}\right|+1\right)$
38 37 rabbidv ${⊢}{b}=\left|{c}\right|+1\to \left\{{a}\in {W}|\left|{a}\right|<{b}\right\}=\left\{{a}\in {W}|\left|{a}\right|<\left|{c}\right|+1\right\}$
39 38 sseq1d ${⊢}{b}=\left|{c}\right|+1\to \left(\left\{{a}\in {W}|\left|{a}\right|<{b}\right\}\subseteq \mathrm{ran}{S}↔\left\{{a}\in {W}|\left|{a}\right|<\left|{c}\right|+1\right\}\subseteq \mathrm{ran}{S}\right)$
40 0ss ${⊢}\varnothing \subseteq \mathrm{ran}{S}$
41 simpr ${⊢}\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\to \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}$
42 fveqeq2 ${⊢}{a}={c}\to \left(\left|{a}\right|={d}↔\left|{c}\right|={d}\right)$
43 42 cbvrabv ${⊢}\left\{{a}\in {W}|\left|{a}\right|={d}\right\}=\left\{{c}\in {W}|\left|{c}\right|={d}\right\}$
44 eliun ${⊢}{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)↔\exists {x}\in {W}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{ran}{T}\left({x}\right)$
45 fveq2 ${⊢}{x}={b}\to {T}\left({x}\right)={T}\left({b}\right)$
46 45 rneqd ${⊢}{x}={b}\to \mathrm{ran}{T}\left({x}\right)=\mathrm{ran}{T}\left({b}\right)$
47 46 eleq2d ${⊢}{x}={b}\to \left({c}\in \mathrm{ran}{T}\left({x}\right)↔{c}\in \mathrm{ran}{T}\left({b}\right)\right)$
48 47 cbvrexvw ${⊢}\exists {x}\in {W}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{ran}{T}\left({x}\right)↔\exists {b}\in {W}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{ran}{T}\left({b}\right)$
49 44 48 bitri ${⊢}{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)↔\exists {b}\in {W}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{ran}{T}\left({b}\right)$
50 simpl1r ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}$
51 fveq2 ${⊢}{a}={b}\to \left|{a}\right|=\left|{b}\right|$
52 51 breq1d ${⊢}{a}={b}\to \left(\left|{a}\right|<{d}↔\left|{b}\right|<{d}\right)$
53 simprl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to {b}\in {W}$
54 14 53 sseldi ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to {b}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
55 lencl ${⊢}{b}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{b}\right|\in {ℕ}_{0}$
56 54 55 syl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{b}\right|\in {ℕ}_{0}$
57 56 nn0red ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{b}\right|\in ℝ$
58 2rp ${⊢}2\in {ℝ}^{+}$
59 ltaddrp ${⊢}\left(\left|{b}\right|\in ℝ\wedge 2\in {ℝ}^{+}\right)\to \left|{b}\right|<\left|{b}\right|+2$
60 57 58 59 sylancl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{b}\right|<\left|{b}\right|+2$
61 1 2 3 4 efgtlen ${⊢}\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\to \left|{c}\right|=\left|{b}\right|+2$
62 61 adantl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{c}\right|=\left|{b}\right|+2$
63 simpl3 ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{c}\right|={d}$
64 62 63 eqtr3d ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{b}\right|+2={d}$
65 60 64 breqtrd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \left|{b}\right|<{d}$
66 52 53 65 elrabd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to {b}\in \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}$
67 50 66 sseldd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to {b}\in \mathrm{ran}{S}$
68 ffn ${⊢}{S}:\mathrm{dom}{S}⟶{W}\to {S}Fn\mathrm{dom}{S}$
69 10 68 ax-mp ${⊢}{S}Fn\mathrm{dom}{S}$
70 fvelrnb ${⊢}{S}Fn\mathrm{dom}{S}\to \left({b}\in \mathrm{ran}{S}↔\exists {o}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}{S}\left({o}\right)={b}\right)$
71 69 70 ax-mp ${⊢}{b}\in \mathrm{ran}{S}↔\exists {o}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}{S}\left({o}\right)={b}$
72 67 71 sylib ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to \exists {o}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}{S}\left({o}\right)={b}$
73 simprrl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {o}\in \mathrm{dom}{S}$
74 1 2 3 4 5 6 efgsdm ${⊢}{o}\in \mathrm{dom}{S}↔\left({o}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)\wedge {o}\left(0\right)\in {D}\wedge \forall {i}\in \left(1..^\left|{o}\right|\right)\phantom{\rule{.4em}{0ex}}{o}\left({i}\right)\in \mathrm{ran}{T}\left({o}\left({i}-1\right)\right)\right)$
75 74 simp1bi ${⊢}{o}\in \mathrm{dom}{S}\to {o}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)$
76 eldifi ${⊢}{o}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)\to {o}\in \mathrm{Word}{W}$
77 73 75 76 3syl ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {o}\in \mathrm{Word}{W}$
78 simpl2 ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {c}\in {W}$
79 simprlr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {c}\in \mathrm{ran}{T}\left({b}\right)$
80 simprrr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {S}\left({o}\right)={b}$
81 80 fveq2d ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {T}\left({S}\left({o}\right)\right)={T}\left({b}\right)$
82 81 rneqd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to \mathrm{ran}{T}\left({S}\left({o}\right)\right)=\mathrm{ran}{T}\left({b}\right)$
83 79 82 eleqtrrd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {c}\in \mathrm{ran}{T}\left({S}\left({o}\right)\right)$
84 1 2 3 4 5 6 efgsp1 ${⊢}\left({o}\in \mathrm{dom}{S}\wedge {c}\in \mathrm{ran}{T}\left({S}\left({o}\right)\right)\right)\to {o}\mathrm{++}⟨“{c}”⟩\in \mathrm{dom}{S}$
85 73 83 84 syl2anc ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {o}\mathrm{++}⟨“{c}”⟩\in \mathrm{dom}{S}$
86 1 2 3 4 5 6 efgsval2 ${⊢}\left({o}\in \mathrm{Word}{W}\wedge {c}\in {W}\wedge {o}\mathrm{++}⟨“{c}”⟩\in \mathrm{dom}{S}\right)\to {S}\left({o}\mathrm{++}⟨“{c}”⟩\right)={c}$
87 77 78 85 86 syl3anc ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {S}\left({o}\mathrm{++}⟨“{c}”⟩\right)={c}$
88 fnfvelrn ${⊢}\left({S}Fn\mathrm{dom}{S}\wedge {o}\mathrm{++}⟨“{c}”⟩\in \mathrm{dom}{S}\right)\to {S}\left({o}\mathrm{++}⟨“{c}”⟩\right)\in \mathrm{ran}{S}$
89 69 85 88 sylancr ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {S}\left({o}\mathrm{++}⟨“{c}”⟩\right)\in \mathrm{ran}{S}$
90 87 89 eqeltrrd ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left(\left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\right)\to {c}\in \mathrm{ran}{S}$
91 90 anassrs ${⊢}\left(\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\wedge \left({o}\in \mathrm{dom}{S}\wedge {S}\left({o}\right)={b}\right)\right)\to {c}\in \mathrm{ran}{S}$
92 72 91 rexlimddv ${⊢}\left(\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\wedge \left({b}\in {W}\wedge {c}\in \mathrm{ran}{T}\left({b}\right)\right)\right)\to {c}\in \mathrm{ran}{S}$
93 92 rexlimdvaa ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\to \left(\exists {b}\in {W}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{ran}{T}\left({b}\right)\to {c}\in \mathrm{ran}{S}\right)$
94 49 93 syl5bi ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\to \left({c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\to {c}\in \mathrm{ran}{S}\right)$
95 eldif ${⊢}{c}\in \left({W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)↔\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)$
96 5 eleq2i ${⊢}{c}\in {D}↔{c}\in \left({W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)$
97 1 2 3 4 5 6 efgs1 ${⊢}{c}\in {D}\to ⟨“{c}”⟩\in \mathrm{dom}{S}$
98 96 97 sylbir ${⊢}{c}\in \left({W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to ⟨“{c}”⟩\in \mathrm{dom}{S}$
99 95 98 sylbir ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to ⟨“{c}”⟩\in \mathrm{dom}{S}$
100 1 2 3 4 5 6 efgsval ${⊢}⟨“{c}”⟩\in \mathrm{dom}{S}\to {S}\left(⟨“{c}”⟩\right)=⟨“{c}”⟩\left(\left|⟨“{c}”⟩\right|-1\right)$
101 99 100 syl ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to {S}\left(⟨“{c}”⟩\right)=⟨“{c}”⟩\left(\left|⟨“{c}”⟩\right|-1\right)$
102 s1len ${⊢}\left|⟨“{c}”⟩\right|=1$
103 102 oveq1i ${⊢}\left|⟨“{c}”⟩\right|-1=1-1$
104 1m1e0 ${⊢}1-1=0$
105 103 104 eqtri ${⊢}\left|⟨“{c}”⟩\right|-1=0$
106 105 fveq2i ${⊢}⟨“{c}”⟩\left(\left|⟨“{c}”⟩\right|-1\right)=⟨“{c}”⟩\left(0\right)$
107 106 a1i ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to ⟨“{c}”⟩\left(\left|⟨“{c}”⟩\right|-1\right)=⟨“{c}”⟩\left(0\right)$
108 s1fv ${⊢}{c}\in {W}\to ⟨“{c}”⟩\left(0\right)={c}$
109 108 adantr ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to ⟨“{c}”⟩\left(0\right)={c}$
110 101 107 109 3eqtrd ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to {S}\left(⟨“{c}”⟩\right)={c}$
111 fnfvelrn ${⊢}\left({S}Fn\mathrm{dom}{S}\wedge ⟨“{c}”⟩\in \mathrm{dom}{S}\right)\to {S}\left(⟨“{c}”⟩\right)\in \mathrm{ran}{S}$
112 69 99 111 sylancr ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to {S}\left(⟨“{c}”⟩\right)\in \mathrm{ran}{S}$
113 110 112 eqeltrrd ${⊢}\left({c}\in {W}\wedge ¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\right)\to {c}\in \mathrm{ran}{S}$
114 113 ex ${⊢}{c}\in {W}\to \left(¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\to {c}\in \mathrm{ran}{S}\right)$
115 114 3ad2ant2 ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\to \left(¬{c}\in \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)\to {c}\in \mathrm{ran}{S}\right)$
116 94 115 pm2.61d ${⊢}\left(\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\wedge {c}\in {W}\wedge \left|{c}\right|={d}\right)\to {c}\in \mathrm{ran}{S}$
117 116 rabssdv ${⊢}\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\to \left\{{c}\in {W}|\left|{c}\right|={d}\right\}\subseteq \mathrm{ran}{S}$
118 43 117 eqsstrid ${⊢}\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\to \left\{{a}\in {W}|\left|{a}\right|={d}\right\}\subseteq \mathrm{ran}{S}$
119 41 118 unssd ${⊢}\left({d}\in {ℕ}_{0}\wedge \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\right)\to \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\cup \left\{{a}\in {W}|\left|{a}\right|={d}\right\}\subseteq \mathrm{ran}{S}$
120 119 ex ${⊢}{d}\in {ℕ}_{0}\to \left(\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\to \left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\cup \left\{{a}\in {W}|\left|{a}\right|={d}\right\}\subseteq \mathrm{ran}{S}\right)$
121 id ${⊢}{d}\in {ℕ}_{0}\to {d}\in {ℕ}_{0}$
122 nn0leltp1 ${⊢}\left(\left|{a}\right|\in {ℕ}_{0}\wedge {d}\in {ℕ}_{0}\right)\to \left(\left|{a}\right|\le {d}↔\left|{a}\right|<{d}+1\right)$
123 21 121 122 syl2anr ${⊢}\left({d}\in {ℕ}_{0}\wedge {a}\in {W}\right)\to \left(\left|{a}\right|\le {d}↔\left|{a}\right|<{d}+1\right)$
124 21 nn0red ${⊢}{a}\in {W}\to \left|{a}\right|\in ℝ$
125 nn0re ${⊢}{d}\in {ℕ}_{0}\to {d}\in ℝ$
126 leloe ${⊢}\left(\left|{a}\right|\in ℝ\wedge {d}\in ℝ\right)\to \left(\left|{a}\right|\le {d}↔\left(\left|{a}\right|<{d}\vee \left|{a}\right|={d}\right)\right)$
127 124 125 126 syl2anr ${⊢}\left({d}\in {ℕ}_{0}\wedge {a}\in {W}\right)\to \left(\left|{a}\right|\le {d}↔\left(\left|{a}\right|<{d}\vee \left|{a}\right|={d}\right)\right)$
128 123 127 bitr3d ${⊢}\left({d}\in {ℕ}_{0}\wedge {a}\in {W}\right)\to \left(\left|{a}\right|<{d}+1↔\left(\left|{a}\right|<{d}\vee \left|{a}\right|={d}\right)\right)$
129 128 rabbidva ${⊢}{d}\in {ℕ}_{0}\to \left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}=\left\{{a}\in {W}|\left(\left|{a}\right|<{d}\vee \left|{a}\right|={d}\right)\right\}$
130 unrab ${⊢}\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\cup \left\{{a}\in {W}|\left|{a}\right|={d}\right\}=\left\{{a}\in {W}|\left(\left|{a}\right|<{d}\vee \left|{a}\right|={d}\right)\right\}$
131 129 130 syl6eqr ${⊢}{d}\in {ℕ}_{0}\to \left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}=\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\cup \left\{{a}\in {W}|\left|{a}\right|={d}\right\}$
132 131 sseq1d ${⊢}{d}\in {ℕ}_{0}\to \left(\left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}\subseteq \mathrm{ran}{S}↔\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\cup \left\{{a}\in {W}|\left|{a}\right|={d}\right\}\subseteq \mathrm{ran}{S}\right)$
133 120 132 sylibrd ${⊢}{d}\in {ℕ}_{0}\to \left(\left\{{a}\in {W}|\left|{a}\right|<{d}\right\}\subseteq \mathrm{ran}{S}\to \left\{{a}\in {W}|\left|{a}\right|<{d}+1\right\}\subseteq \mathrm{ran}{S}\right)$
134 30 33 36 39 40 133 nn0ind ${⊢}\left|{c}\right|+1\in {ℕ}_{0}\to \left\{{a}\in {W}|\left|{a}\right|<\left|{c}\right|+1\right\}\subseteq \mathrm{ran}{S}$
135 17 18 134 3syl ${⊢}{c}\in {W}\to \left\{{a}\in {W}|\left|{a}\right|<\left|{c}\right|+1\right\}\subseteq \mathrm{ran}{S}$
136 fveq2 ${⊢}{a}={c}\to \left|{a}\right|=\left|{c}\right|$
137 136 breq1d ${⊢}{a}={c}\to \left(\left|{a}\right|<\left|{c}\right|+1↔\left|{c}\right|<\left|{c}\right|+1\right)$
138 id ${⊢}{c}\in {W}\to {c}\in {W}$
139 17 nn0red ${⊢}{c}\in {W}\to \left|{c}\right|\in ℝ$
140 139 ltp1d ${⊢}{c}\in {W}\to \left|{c}\right|<\left|{c}\right|+1$
141 137 138 140 elrabd ${⊢}{c}\in {W}\to {c}\in \left\{{a}\in {W}|\left|{a}\right|<\left|{c}\right|+1\right\}$
142 135 141 sseldd ${⊢}{c}\in {W}\to {c}\in \mathrm{ran}{S}$
143 142 ssriv ${⊢}{W}\subseteq \mathrm{ran}{S}$
144 12 143 eqssi ${⊢}\mathrm{ran}{S}={W}$
145 dffo2 ${⊢}{S}:\mathrm{dom}{S}\underset{onto}{⟶}{W}↔\left({S}:\mathrm{dom}{S}⟶{W}\wedge \mathrm{ran}{S}={W}\right)$
146 10 144 145 mpbir2an ${⊢}{S}:\mathrm{dom}{S}\underset{onto}{⟶}{W}$