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 ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
efgcpbllem.1 ⊢ 𝐿 = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑊 ∧ ( ( 𝐴 ++ 𝑖 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑗 ) ++ 𝐵 ) ) }
Assertion efgcpbllemb ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∼ ⊆ 𝐿 )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 efgcpbllem.1 ⊢ 𝐿 = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑊 ∧ ( ( 𝐴 ++ 𝑖 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑗 ) ++ 𝐵 ) ) }
8 1 2 3 4 efgval2 ⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) }
9 7 relopabi ⊢ Rel 𝐿
10 9 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → Rel 𝐿 )
11 1 2 3 4 5 6 7 efgcpbllema ⊢ ( 𝑓 𝐿 𝑔 ↔ ( 𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ) )
12 11 simp2bi ⊢ ( 𝑓 𝐿 𝑔 → 𝑔 ∈ 𝑊 )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑔 ∈ 𝑊 )
14 11 simp1bi ⊢ ( 𝑓 𝐿 𝑔 → 𝑓 ∈ 𝑊 )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑓 ∈ 𝑊 )
16 1 2 efger ⊢ ∼ Er 𝑊
17 16 a1i ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ∼ Er 𝑊 )
18 11 simp3bi ⊢ ( 𝑓 𝐿 𝑔 → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) )
20 17 19 ersym ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) )
21 1 2 3 4 5 6 7 efgcpbllema ⊢ ( 𝑔 𝐿 𝑓 ↔ ( 𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
22 13 15 20 21 syl3anbrc ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑔 𝐿 𝑓 )
23 14 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → 𝑓 ∈ 𝑊 )
24 1 2 3 4 5 6 7 efgcpbllema ⊢ ( 𝑔 𝐿 ℎ ↔ ( 𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) )
25 24 simp2bi ⊢ ( 𝑔 𝐿 ℎ → ℎ ∈ 𝑊 )
26 25 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ℎ ∈ 𝑊 )
27 16 a1i ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ∼ Er 𝑊 )
28 18 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) )
29 24 simp3bi ⊢ ( 𝑔 𝐿 ℎ → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) )
30 29 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) )
31 27 28 30 ertrd ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) )
32 1 2 3 4 5 6 7 efgcpbllema ⊢ ( 𝑓 𝐿 ℎ ↔ ( 𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) )
33 23 26 31 32 syl3anbrc ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → 𝑓 𝐿 ℎ )
34 16 a1i ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ∼ Er 𝑊 )
35 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
36 1 35 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
37 simpll ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ 𝑊 )
38 36 37 sseldi ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ Word ( 𝐼 × 2o ) )
39 simpr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ 𝑊 )
40 36 39 sseldi ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ Word ( 𝐼 × 2o ) )
41 ccatcl ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2o ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) )
42 38 40 41 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) )
43 simplr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
44 36 43 sseldi ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ Word ( 𝐼 × 2o ) )
45 ccatcl ⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) )
46 42 44 45 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) )
47 1 efgrcl ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
48 47 simprd ⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
49 48 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2o ) )
50 46 49 eleqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 )
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 ⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ) ↔ 𝑓 ∈ 𝑊 )
57 56 anbi1i ⊢ ( ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ) ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ↔ ( 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
58 54 55 57 3bitri ⊢ ( 𝑓 𝐿 𝑓 ↔ ( 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
59 53 58 bitr4di ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝑊 ↔ 𝑓 𝐿 𝑓 ) )
60 10 22 33 59 iserd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 Er 𝑊 )
61 1 2 3 4 efgtf ⊢ ( 𝑓 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑓 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑓 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
62 61 simprd ⊢ ( 𝑓 ∈ 𝑊 → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
63 62 adantl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
64 ffn ⊢ ( ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) )
65 ovelrn ⊢ ( ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
66 63 64 65 3syl ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
67 simplr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 ∈ 𝑊 )
68 62 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
69 simprl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
70 simprr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑢 ∈ ( 𝐼 × 2o ) )
71 68 69 70 fovrnd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 )
72 50 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 )
73 37 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐴 ∈ 𝑊 )
74 36 73 sseldi ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐴 ∈ Word ( 𝐼 × 2o ) )
75 40 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 ∈ Word ( 𝐼 × 2o ) )
76 pfxcl ⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) )
77 75 76 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) )
78 ccatcl ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) )
79 74 77 78 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) )
80 3 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
81 80 ffvelrni ⊢ ( 𝑢 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2o ) )
82 81 ad2antll ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2o ) )
83 70 82 s2cld ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
84 ccatcl ⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
85 79 83 84 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
86 swrdcl ⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
87 75 86 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
88 44 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐵 ∈ Word ( 𝐼 × 2o ) )
89 ccatass ⊢ ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
90 85 87 88 89 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
91 ccatcl ⊢ ( ( ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
92 77 83 91 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
93 ccatass ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
94 74 92 87 93 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
95 ccatass ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) )
96 74 77 83 95 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) )
97 96 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
98 1 2 3 4 efgtval ⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
99 67 69 70 98 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
100 splval ⊢ ( ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ) → ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
101 67 69 69 83 100 syl13anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
102 99 101 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
103 102 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
104 94 97 103 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
105 104 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) )
106 lencl ⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
107 74 106 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
108 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
109 107 108 eleqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
110 elfznn0 ⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → 𝑐 ∈ ℕ0 )
111 110 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ℕ0 )
112 uzaddcl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑐 ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) )
113 109 111 112 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) )
114 42 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) )
115 ccatlen ⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) )
116 114 88 115 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) )
117 ccatlen ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
118 74 75 117 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
119 elfzuz3 ⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) )
120 119 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) )
121 107 nn0zd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
122 eluzadd ⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) )
123 120 121 122 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) )
124 lencl ⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
125 75 124 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
126 125 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℂ )
127 107 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
128 126 127 addcomd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
129 111 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ℂ )
130 129 127 addcomd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
131 130 fveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
132 123 128 131 3eltr3d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
133 118 132 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
134 lencl ⊢ ( 𝐵 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
135 88 134 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
136 uzaddcl ⊢ ( ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
137 133 135 136 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
138 116 137 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
139 elfzuzb ⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) )
140 113 138 139 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) )
141 1 2 3 4 efgtval ⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
142 72 140 70 141 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
143 wrd0 ⊢ ∅ ∈ Word ( 𝐼 × 2o )
144 143 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ∅ ∈ Word ( 𝐼 × 2o ) )
145 ccatcl ⊢ ( ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) )
146 87 88 145 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) )
147 ccatrid ⊢ ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) )
148 79 147 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) )
149 148 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
150 ccatass ⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
151 79 87 88 150 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
152 ccatass ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
153 74 77 87 152 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
154 125 108 eleqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 0 ) )
155 eluzfz2 ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
156 154 155 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
157 ccatpfx ⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) )
158 75 69 156 157 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) )
159 pfxid ⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 )
160 75 159 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 )
161 158 160 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = 𝑓 )
162 161 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) = ( 𝐴 ++ 𝑓 ) )
163 153 162 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ 𝑓 ) )
164 163 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) )
165 149 151 164 3eqtr2rd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
166 ccatlen ⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) )
167 74 77 166 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) )
168 pfxlen ⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 )
169 75 69 168 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 )
170 169 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
171 167 170 eqtr2d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) )
172 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
173 172 oveq2i ⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 )
174 107 111 nn0addcld ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℕ0 )
175 174 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℂ )
176 175 addid1d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
177 173 176 syl5req ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) )
178 79 144 146 83 165 171 177 splval2 ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
179 142 178 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
180 90 105 179 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) )
181 1 2 3 4 efgtf ⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
182 181 simprd ⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
183 ffn ⊢ ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) )
184 72 182 183 3syl ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) )
185 fnovrn ⊢ ( ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
186 184 140 70 185 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
187 180 186 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
188 1 2 3 4 efgi2 ⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) )
189 72 187 188 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) )
190 1 2 3 4 5 6 7 efgcpbllema ⊢ ( 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ↔ ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ) )
191 67 71 189 190 syl3anbrc ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) )
192 vex ⊢ 𝑎 ∈ V
193 vex ⊢ 𝑓 ∈ V
194 192 193 elec ⊢ ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 𝑎 )
195 breq2 ⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑓 𝐿 𝑎 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
196 194 195 syl5bb ⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
197 191 196 syl5ibrcom ⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) )
198 197 rexlimdvva ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) )
199 66 198 sylbid ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) )
200 199 ssrdv ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 )
201 200 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 )
202 1 fvexi ⊢ 𝑊 ∈ V
203 erex ⊢ ( 𝐿 Er 𝑊 → ( 𝑊 ∈ V → 𝐿 ∈ V ) )
204 60 202 203 mpisyl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 ∈ V )
205 ereq1 ⊢ ( 𝑟 = 𝐿 → ( 𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊 ) )
206 eceq2 ⊢ ( 𝑟 = 𝐿 → [ 𝑓 ] 𝑟 = [ 𝑓 ] 𝐿 )
207 206 sseq2d ⊢ ( 𝑟 = 𝐿 → ( ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ↔ ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) )
208 207 ralbidv ⊢ ( 𝑟 = 𝐿 → ( ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ↔ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) )
209 205 208 anbi12d ⊢ ( 𝑟 = 𝐿 → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) )
210 209 elabg ⊢ ( 𝐿 ∈ V → ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) )
211 204 210 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) )
212 60 201 211 mpbir2and ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } )
213 intss1 ⊢ ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ⊆ 𝐿 )
214 212 213 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ⊆ 𝐿 )
215 8 214 eqsstrid ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∼ ⊆ 𝐿 )