# Metamath Proof Explorer

## Theorem efgcpbllemb

Description: Lemma for efgrelex . Show that L is an equivalence relation containing all direct extensions of a word, so is closed under .~ . (Contributed by Mario Carneiro, 1-Oct-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)$
efgcpbllem.1
Assertion efgcpbllemb

### 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 efgcpbllem.1
8 1 2 3 4 efgval2
9 7 relopabi ${⊢}\mathrm{Rel}{L}$
10 9 a1i ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \mathrm{Rel}{L}$
11 1 2 3 4 5 6 7 efgcpbllema
12 11 simp2bi ${⊢}{f}{L}{g}\to {g}\in {W}$
13 12 adantl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}{L}{g}\right)\to {g}\in {W}$
14 11 simp1bi ${⊢}{f}{L}{g}\to {f}\in {W}$
15 14 adantl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}{L}{g}\right)\to {f}\in {W}$
16 1 2 efger
17 16 a1i
18 11 simp3bi
20 17 19 ersym
21 1 2 3 4 5 6 7 efgcpbllema
22 13 15 20 21 syl3anbrc ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}{L}{g}\right)\to {g}{L}{f}$
23 14 ad2antrl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({f}{L}{g}\wedge {g}{L}{h}\right)\right)\to {f}\in {W}$
24 1 2 3 4 5 6 7 efgcpbllema
25 24 simp2bi ${⊢}{g}{L}{h}\to {h}\in {W}$
26 25 ad2antll ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({f}{L}{g}\wedge {g}{L}{h}\right)\right)\to {h}\in {W}$
27 16 a1i
29 24 simp3bi
31 27 28 30 ertrd
32 1 2 3 4 5 6 7 efgcpbllema
33 23 26 31 32 syl3anbrc ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge \left({f}{L}{g}\wedge {g}{L}{h}\right)\right)\to {f}{L}{h}$
34 16 a1i
35 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
36 1 35 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
37 simpll ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {A}\in {W}$
38 36 37 sseldi ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
39 simpr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {f}\in {W}$
40 36 39 sseldi ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
41 ccatcl ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {A}\mathrm{++}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
42 38 40 41 syl2anc ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {A}\mathrm{++}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
43 simplr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {B}\in {W}$
44 36 43 sseldi ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
45 ccatcl ${⊢}\left({A}\mathrm{++}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
46 42 44 45 syl2anc ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
47 1 efgrcl ${⊢}{A}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
48 47 simprd ${⊢}{A}\in {W}\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
49 48 ad2antrr ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
50 46 49 eleqtrrd ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in {W}$
51 34 50 erref
52 51 ex
53 52 pm4.71d
54 1 2 3 4 5 6 7 efgcpbllema
55 df-3an
56 anidm ${⊢}\left({f}\in {W}\wedge {f}\in {W}\right)↔{f}\in {W}$
57 56 anbi1i
58 54 55 57 3bitri
59 53 58 syl6bbr ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \left({f}\in {W}↔{f}{L}{f}\right)$
60 10 22 33 59 iserd ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {L}\mathrm{Er}{W}$
61 1 2 3 4 efgtf ${⊢}{f}\in {W}\to \left({T}\left({f}\right)=\left({a}\in \left(0\dots \left|{f}\right|\right),{b}\in \left({I}×{2}_{𝑜}\right)⟼{f}\mathrm{splice}⟨{a},{a},⟨“{b}{M}\left({b}\right)”⟩⟩\right)\wedge {T}\left({f}\right):\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}\right)$
62 61 simprd ${⊢}{f}\in {W}\to {T}\left({f}\right):\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}$
63 62 adantl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to {T}\left({f}\right):\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}$
64 ffn ${⊢}{T}\left({f}\right):\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}\to {T}\left({f}\right)Fn\left(\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)\right)$
65 ovelrn ${⊢}{T}\left({f}\right)Fn\left(\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)\right)\to \left({a}\in \mathrm{ran}{T}\left({f}\right)↔\exists {c}\in \left(0\dots \left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({I}×{2}_{𝑜}\right)\phantom{\rule{.4em}{0ex}}{a}={c}{T}\left({f}\right){u}\right)$
66 63 64 65 3syl ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \left({a}\in \mathrm{ran}{T}\left({f}\right)↔\exists {c}\in \left(0\dots \left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({I}×{2}_{𝑜}\right)\phantom{\rule{.4em}{0ex}}{a}={c}{T}\left({f}\right){u}\right)$
67 simplr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\in {W}$
68 62 ad2antlr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {T}\left({f}\right):\left(0\dots \left|{f}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}$
69 simprl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}\in \left(0\dots \left|{f}\right|\right)$
70 simprr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {u}\in \left({I}×{2}_{𝑜}\right)$
71 68 69 70 fovrnd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}{T}\left({f}\right){u}\in {W}$
72 50 adantr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in {W}$
73 37 adantr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\in {W}$
74 36 73 sseldi ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
75 40 adantr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
76 pfxcl ${⊢}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
77 75 76 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
78 ccatcl ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
79 74 77 78 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
80 3 efgmf ${⊢}{M}:{I}×{2}_{𝑜}⟶{I}×{2}_{𝑜}$
81 80 ffvelrni ${⊢}{u}\in \left({I}×{2}_{𝑜}\right)\to {M}\left({u}\right)\in \left({I}×{2}_{𝑜}\right)$
82 81 ad2antll ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {M}\left({u}\right)\in \left({I}×{2}_{𝑜}\right)$
83 70 82 s2cld ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to ⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
84 ccatcl ${⊢}\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge ⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
85 79 83 84 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
86 swrdcl ${⊢}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
87 75 86 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
88 44 adantr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
89 ccatass ${⊢}\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left(\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
90 85 87 88 89 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
91 ccatcl ${⊢}\left({f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge ⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
92 77 83 91 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
93 ccatass ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge \left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={A}\mathrm{++}\left(\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)$
94 74 92 87 93 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={A}\mathrm{++}\left(\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)$
95 ccatass ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge ⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩={A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)$
96 74 77 83 95 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩={A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)$
97 96 oveq1d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)=\left({A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)$
98 1 2 3 4 efgtval ${⊢}\left({f}\in {W}\wedge {c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\to {c}{T}\left({f}\right){u}={f}\mathrm{splice}⟨{c},{c},⟨“{u}{M}\left({u}\right)”⟩⟩$
99 67 69 70 98 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}{T}\left({f}\right){u}={f}\mathrm{splice}⟨{c},{c},⟨“{u}{M}\left({u}\right)”⟩⟩$
100 splval ${⊢}\left({f}\in {W}\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {c}\in \left(0\dots \left|{f}\right|\right)\wedge ⟨“{u}{M}\left({u}\right)”⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\mathrm{splice}⟨{c},{c},⟨“{u}{M}\left({u}\right)”⟩⟩=\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)$
101 67 69 69 83 100 syl13anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\mathrm{splice}⟨{c},{c},⟨“{u}{M}\left({u}\right)”⟩⟩=\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)$
102 99 101 eqtrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}{T}\left({f}\right){u}=\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)$
103 102 oveq2d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\mathrm{++}\left({c}{T}\left({f}\right){u}\right)={A}\mathrm{++}\left(\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)$
104 94 97 103 3eqtr4rd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\mathrm{++}\left({c}{T}\left({f}\right){u}\right)=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)$
105 104 oveq1d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({c}{T}\left({f}\right){u}\right)\right)\mathrm{++}{B}=\left(\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}$
106 lencl ${⊢}{A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{A}\right|\in {ℕ}_{0}$
107 74 106 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|\in {ℕ}_{0}$
108 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
109 107 108 eleqtrdi ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|\in {ℤ}_{\ge 0}$
110 elfznn0 ${⊢}{c}\in \left(0\dots \left|{f}\right|\right)\to {c}\in {ℕ}_{0}$
111 110 ad2antrl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}\in {ℕ}_{0}$
112 uzaddcl ${⊢}\left(\left|{A}\right|\in {ℤ}_{\ge 0}\wedge {c}\in {ℕ}_{0}\right)\to \left|{A}\right|+{c}\in {ℤ}_{\ge 0}$
113 109 111 112 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}\in {ℤ}_{\ge 0}$
114 42 adantr ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\mathrm{++}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
115 ccatlen ${⊢}\left({A}\mathrm{++}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|=\left|{A}\mathrm{++}{f}\right|+\left|{B}\right|$
116 114 88 115 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|=\left|{A}\mathrm{++}{f}\right|+\left|{B}\right|$
117 ccatlen ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left|{A}\mathrm{++}{f}\right|=\left|{A}\right|+\left|{f}\right|$
118 74 75 117 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\mathrm{++}{f}\right|=\left|{A}\right|+\left|{f}\right|$
119 elfzuz3 ${⊢}{c}\in \left(0\dots \left|{f}\right|\right)\to \left|{f}\right|\in {ℤ}_{\ge {c}}$
120 119 ad2antrl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|\in {ℤ}_{\ge {c}}$
121 107 nn0zd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|\in ℤ$
122 eluzadd ${⊢}\left(\left|{f}\right|\in {ℤ}_{\ge {c}}\wedge \left|{A}\right|\in ℤ\right)\to \left|{f}\right|+\left|{A}\right|\in {ℤ}_{\ge \left({c}+\left|{A}\right|\right)}$
123 120 121 122 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|+\left|{A}\right|\in {ℤ}_{\ge \left({c}+\left|{A}\right|\right)}$
124 lencl ${⊢}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{f}\right|\in {ℕ}_{0}$
125 75 124 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|\in {ℕ}_{0}$
126 125 nn0cnd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|\in ℂ$
127 107 nn0cnd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|\in ℂ$
128 126 127 addcomd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|+\left|{A}\right|=\left|{A}\right|+\left|{f}\right|$
129 111 nn0cnd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}\in ℂ$
130 129 127 addcomd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {c}+\left|{A}\right|=\left|{A}\right|+{c}$
131 130 fveq2d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {ℤ}_{\ge \left({c}+\left|{A}\right|\right)}={ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
132 123 128 131 3eltr3d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+\left|{f}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
133 118 132 eqeltrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\mathrm{++}{f}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
134 lencl ${⊢}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{B}\right|\in {ℕ}_{0}$
135 88 134 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{B}\right|\in {ℕ}_{0}$
136 uzaddcl ${⊢}\left(\left|{A}\mathrm{++}{f}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left|{A}\mathrm{++}{f}\right|+\left|{B}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
137 133 135 136 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\mathrm{++}{f}\right|+\left|{B}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
138 116 137 eqeltrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}$
139 elfzuzb ${⊢}\left|{A}\right|+{c}\in \left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)↔\left(\left|{A}\right|+{c}\in {ℤ}_{\ge 0}\wedge \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\in {ℤ}_{\ge \left(\left|{A}\right|+{c}\right)}\right)$
140 113 138 139 sylanbrc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}\in \left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)$
141 1 2 3 4 efgtval ${⊢}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in {W}\wedge \left|{A}\right|+{c}\in \left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\to \left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}=\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)\mathrm{splice}⟨\left|{A}\right|+{c},\left|{A}\right|+{c},⟨“{u}{M}\left({u}\right)”⟩⟩$
142 72 140 70 141 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}=\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)\mathrm{splice}⟨\left|{A}\right|+{c},\left|{A}\right|+{c},⟨“{u}{M}\left({u}\right)”⟩⟩$
143 wrd0 ${⊢}\varnothing \in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
144 143 a1i ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \varnothing \in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
145 ccatcl ${⊢}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
146 87 88 145 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
147 ccatrid ${⊢}{A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\varnothing ={A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)$
148 79 147 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\varnothing ={A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)$
149 148 oveq1d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\varnothing \right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)=\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
150 ccatass ${⊢}\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {B}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}=\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
151 79 87 88 150 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}=\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
152 ccatass ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)$
153 74 77 87 152 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)$
154 125 108 eleqtrdi ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|\in {ℤ}_{\ge 0}$
155 eluzfz2 ${⊢}\left|{f}\right|\in {ℤ}_{\ge 0}\to \left|{f}\right|\in \left(0\dots \left|{f}\right|\right)$
156 154 155 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\right|\in \left(0\dots \left|{f}\right|\right)$
157 ccatpfx ${⊢}\left({f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {c}\in \left(0\dots \left|{f}\right|\right)\wedge \left|{f}\right|\in \left(0\dots \left|{f}\right|\right)\right)\to \left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={f}\mathrm{prefix}\left|{f}\right|$
158 75 69 156 157 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={f}\mathrm{prefix}\left|{f}\right|$
159 pfxid ${⊢}{f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to {f}\mathrm{prefix}\left|{f}\right|={f}$
160 75 159 syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}\mathrm{prefix}\left|{f}\right|={f}$
161 158 160 eqtrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={f}$
162 161 oveq2d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {A}\mathrm{++}\left(\left({f}\mathrm{prefix}{c}\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)={A}\mathrm{++}{f}$
163 153 162 eqtrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)={A}\mathrm{++}{f}$
164 163 oveq1d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\right)\mathrm{++}{B}=\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}$
165 149 151 164 3eqtr2rd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}{f}\right)\mathrm{++}{B}=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}\varnothing \right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
166 ccatlen ${⊢}\left({A}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {f}\mathrm{prefix}{c}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to \left|{A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right|=\left|{A}\right|+\left|{f}\mathrm{prefix}{c}\right|$
167 74 77 166 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right|=\left|{A}\right|+\left|{f}\mathrm{prefix}{c}\right|$
168 pfxlen ${⊢}\left({f}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {c}\in \left(0\dots \left|{f}\right|\right)\right)\to \left|{f}\mathrm{prefix}{c}\right|={c}$
169 75 69 168 syl2anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{f}\mathrm{prefix}{c}\right|={c}$
170 169 oveq2d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+\left|{f}\mathrm{prefix}{c}\right|=\left|{A}\right|+{c}$
171 167 170 eqtr2d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}=\left|{A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right|$
172 hash0 ${⊢}\left|\varnothing \right|=0$
173 172 oveq2i ${⊢}\left|{A}\right|+{c}+\left|\varnothing \right|=\left|{A}\right|+{c}+0$
174 107 111 nn0addcld ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}\in {ℕ}_{0}$
175 174 nn0cnd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}\in ℂ$
176 175 addid1d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}+0=\left|{A}\right|+{c}$
177 173 176 syl5req ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left|{A}\right|+{c}=\left|{A}\right|+{c}+\left|\varnothing \right|$
178 79 144 146 83 165 171 177 splval2 ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)\mathrm{splice}⟨\left|{A}\right|+{c},\left|{A}\right|+{c},⟨“{u}{M}\left({u}\right)”⟩⟩=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
179 142 178 eqtrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}=\left(\left({A}\mathrm{++}\left({f}\mathrm{prefix}{c}\right)\right)\mathrm{++}⟨“{u}{M}\left({u}\right)”⟩\right)\mathrm{++}\left(\left({f}\mathrm{substr}⟨{c},\left|{f}\right|⟩\right)\mathrm{++}{B}\right)$
180 90 105 179 3eqtr4d ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({c}{T}\left({f}\right){u}\right)\right)\mathrm{++}{B}=\left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}$
181 1 2 3 4 efgtf ${⊢}\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in {W}\to \left({T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)=\left({a}\in \left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right),{b}\in \left({I}×{2}_{𝑜}\right)⟼\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)\mathrm{splice}⟨{a},{a},⟨“{b}{M}\left({b}\right)”⟩⟩\right)\wedge {T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right):\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}\right)$
182 181 simprd ${⊢}\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\in {W}\to {T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right):\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}$
183 ffn ${⊢}{T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right):\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)⟶{W}\to {T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)Fn\left(\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)\right)$
184 72 182 183 3syl ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)Fn\left(\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)\right)$
185 fnovrn ${⊢}\left({T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)Fn\left(\left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)×\left({I}×{2}_{𝑜}\right)\right)\wedge \left|{A}\right|+{c}\in \left(0\dots \left|\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\to \left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}\in \mathrm{ran}{T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)$
186 184 140 70 185 syl3anc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left(\left|{A}\right|+{c}\right){T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right){u}\in \mathrm{ran}{T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)$
187 180 186 eqeltrd ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({A}\mathrm{++}\left({c}{T}\left({f}\right){u}\right)\right)\mathrm{++}{B}\in \mathrm{ran}{T}\left(\left({A}\mathrm{++}{f}\right)\mathrm{++}{B}\right)$
188 1 2 3 4 efgi2
189 72 187 188 syl2anc
190 1 2 3 4 5 6 7 efgcpbllema
191 67 71 189 190 syl3anbrc ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to {f}{L}\left({c}{T}\left({f}\right){u}\right)$
192 vex ${⊢}{a}\in \mathrm{V}$
193 vex ${⊢}{f}\in \mathrm{V}$
194 192 193 elec ${⊢}{a}\in \left[{f}\right]{L}↔{f}{L}{a}$
195 breq2 ${⊢}{a}={c}{T}\left({f}\right){u}\to \left({f}{L}{a}↔{f}{L}\left({c}{T}\left({f}\right){u}\right)\right)$
196 194 195 syl5bb ${⊢}{a}={c}{T}\left({f}\right){u}\to \left({a}\in \left[{f}\right]{L}↔{f}{L}\left({c}{T}\left({f}\right){u}\right)\right)$
197 191 196 syl5ibrcom ${⊢}\left(\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\wedge \left({c}\in \left(0\dots \left|{f}\right|\right)\wedge {u}\in \left({I}×{2}_{𝑜}\right)\right)\right)\to \left({a}={c}{T}\left({f}\right){u}\to {a}\in \left[{f}\right]{L}\right)$
198 197 rexlimdvva ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \left(\exists {c}\in \left(0\dots \left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({I}×{2}_{𝑜}\right)\phantom{\rule{.4em}{0ex}}{a}={c}{T}\left({f}\right){u}\to {a}\in \left[{f}\right]{L}\right)$
199 66 198 sylbid ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \left({a}\in \mathrm{ran}{T}\left({f}\right)\to {a}\in \left[{f}\right]{L}\right)$
200 199 ssrdv ${⊢}\left(\left({A}\in {W}\wedge {B}\in {W}\right)\wedge {f}\in {W}\right)\to \mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}$
201 200 ralrimiva ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}$
202 1 fvexi ${⊢}{W}\in \mathrm{V}$
203 erex ${⊢}{L}\mathrm{Er}{W}\to \left({W}\in \mathrm{V}\to {L}\in \mathrm{V}\right)$
204 60 202 203 mpisyl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {L}\in \mathrm{V}$
205 ereq1 ${⊢}{r}={L}\to \left({r}\mathrm{Er}{W}↔{L}\mathrm{Er}{W}\right)$
206 eceq2 ${⊢}{r}={L}\to \left[{f}\right]{r}=\left[{f}\right]{L}$
207 206 sseq2d ${⊢}{r}={L}\to \left(\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}↔\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}\right)$
208 207 ralbidv ${⊢}{r}={L}\to \left(\forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}↔\forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}\right)$
209 205 208 anbi12d ${⊢}{r}={L}\to \left(\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)↔\left({L}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}\right)\right)$
210 209 elabg ${⊢}{L}\in \mathrm{V}\to \left({L}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}↔\left({L}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}\right)\right)$
211 204 210 syl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \left({L}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}↔\left({L}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{L}\right)\right)$
212 60 201 211 mpbir2and ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to {L}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}$
213 intss1 ${⊢}{L}\in \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}\to \bigcap \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}\subseteq {L}$
214 212 213 syl ${⊢}\left({A}\in {W}\wedge {B}\in {W}\right)\to \bigcap \left\{{r}|\left({r}\mathrm{Er}{W}\wedge \forall {f}\in {W}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{T}\left({f}\right)\subseteq \left[{f}\right]{r}\right)\right\}\subseteq {L}$
215 8 214 eqsstrid