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 ( 𝐼 × 2_o ) )
	efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 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 ( 𝐼 × 2_o ) )
2		efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 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	relopabiv	⊢ 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 ( 𝐼 × 2_o ) ) ⊆ Word ( 𝐼 × 2_o )
36	1 35	eqsstri	⊢ 𝑊 ⊆ Word ( 𝐼 × 2_o )
37		simpll	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ 𝑊 )
38	36 37	sselid	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ Word ( 𝐼 × 2_o ) )
39		simpr	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ 𝑊 )
40	36 39	sselid	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ Word ( 𝐼 × 2_o ) )
41		ccatcl	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2_o ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2_o ) )
42	38 40 41	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2_o ) )
43		simplr	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
44	36 43	sselid	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ Word ( 𝐼 × 2_o ) )
45		ccatcl	⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2_o ) )
46	42 44 45	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2_o ) )
47	1	efgrcl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2_o ) ) )
48	47	simprd	⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2_o ) )
49	48	ad2antrr	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2_o ) )
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 ... ( ♯ ‘ 𝑓 ) ) , 𝑏 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑓 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 ) )
62	61	simprd	⊢ ( 𝑓 ∈ 𝑊 → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 )
63	62	adantl	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 )
64		ffn	⊢ ( ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 → ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) )
65		ovelrn	⊢ ( ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2_o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
66	63 64 65	3syl	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2_o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
67		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑓 ∈ 𝑊 )
68	62	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 )
69		simprl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
70		simprr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑢 ∈ ( 𝐼 × 2_o ) )
71	68 69 70	fovcdmd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 )
72	50	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 )
73	37	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝐴 ∈ 𝑊 )
74	36 73	sselid	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝐴 ∈ Word ( 𝐼 × 2_o ) )
75	40	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑓 ∈ Word ( 𝐼 × 2_o ) )
76		pfxcl	⊢ ( 𝑓 ∈ Word ( 𝐼 × 2_o ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) )
77	75 76	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) )
78		ccatcl	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2_o ) )
79	74 77 78	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2_o ) )
80	3	efgmf	⊢ 𝑀 : ( 𝐼 × 2_o ) ⟶ ( 𝐼 × 2_o )
81	80	ffvelcdmi	⊢ ( 𝑢 ∈ ( 𝐼 × 2_o ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2_o ) )
82	81	ad2antll	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2_o ) )
83	70 82	s2cld	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) )
84		ccatcl	⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2_o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
85	79 83 84	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
86		swrdcl	⊢ ( 𝑓 ∈ Word ( 𝐼 × 2_o ) → ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) )
87	75 86	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) )
88	44	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝐵 ∈ Word ( 𝐼 × 2_o ) )
89		ccatass	⊢ ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2_o ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
90	85 87 88 89	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
91		ccatcl	⊢ ( ( ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
92	77 83 91	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
93		ccatass	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
94	74 92 87 93	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
95		ccatass	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) )
96	74 77 83 95	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) )
97	96	oveq1d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
98	1 2 3 4	efgtval	⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
99	67 69 70 98	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
100		splval	⊢ ( ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) ) ) → ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
101	67 69 69 83 100	syl13anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑓 splice ⟨ 𝑐 , 𝑐 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
102	99 101	eqtrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
103	102	oveq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
104	94 97 103	3eqtr4rd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) )
105	104	oveq1d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) )
106		lencl	⊢ ( 𝐴 ∈ Word ( 𝐼 × 2_o ) → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
107	74 106	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
108		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
109	107 108	eleqtrdi	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 0 ) )
110		elfznn0	⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → 𝑐 ∈ ℕ₀ )
111	110	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑐 ∈ ℕ₀ )
112		uzaddcl	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 0 ) ∧ 𝑐 ∈ ℕ₀ ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ_≥ ‘ 0 ) )
113	109 111 112	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ_≥ ‘ 0 ) )
114	42	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2_o ) )
115		ccatlen	⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2_o ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) )
116	114 88 115	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) )
117		ccatlen	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2_o ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
118	74 75 117	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
119		elfzuz3	⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 𝑐 ) )
120	119	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 𝑐 ) )
121	107	nn0zd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
122		eluzadd	⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 𝑐 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ_≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) )
123	120 121 122	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ_≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) )
124		lencl	⊢ ( 𝑓 ∈ Word ( 𝐼 × 2_o ) → ( ♯ ‘ 𝑓 ) ∈ ℕ₀ )
125	75 124	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℕ₀ )
126	125	nn0cnd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℂ )
127	107	nn0cnd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
128	126 127	addcomd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) )
129	111	nn0cnd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑐 ∈ ℂ )
130	129 127	addcomd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑐 + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
131	130	fveq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ℤ_≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) = ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
132	123 128 131	3eltr3d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
133	118 132	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
134		lencl	⊢ ( 𝐵 ∈ Word ( 𝐼 × 2_o ) → ( ♯ ‘ 𝐵 ) ∈ ℕ₀ )
135	88 134	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ₀ )
136		uzaddcl	⊢ ( ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ₀ ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
137	133 135 136	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
138	116 137	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) )
139		elfzuzb	⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ_≥ ‘ 0 ) ∧ ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) )
140	113 138 139	sylanbrc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) )
141	1 2 3 4	efgtval	⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
142	72 140 70 141	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) )
143		wrd0	⊢ ∅ ∈ Word ( 𝐼 × 2_o )
144	143	a1i	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ∅ ∈ Word ( 𝐼 × 2_o ) )
145		ccatcl	⊢ ( ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2_o ) )
146	87 88 145	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2_o ) )
147		ccatrid	⊢ ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2_o ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) )
148	79 147	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) )
149	148	oveq1d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
150		ccatass	⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2_o ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
151	79 87 88 150	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
152		ccatass	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
153	74 77 87 152	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) )
154	125 108	eleqtrdi	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 0 ) )
155		eluzfz2	⊢ ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ_≥ ‘ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
156	154 155	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) )
157		ccatpfx	⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2_o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) )
158	75 69 156 157	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) )
159		pfxid	⊢ ( 𝑓 ∈ Word ( 𝐼 × 2_o ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 )
160	75 159	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 )
161	158 160	eqtrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = 𝑓 )
162	161	oveq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ) = ( 𝐴 ++ 𝑓 ) )
163	153 162	eqtrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) = ( 𝐴 ++ 𝑓 ) )
164	163	oveq1d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ) ++ 𝐵 ) = ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) )
165	149 151 164	3eqtr2rd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
166		ccatlen	⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2_o ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) )
167	74 77 166	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) )
168		pfxlen	⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2_o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 )
169	75 69 168	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 )
170	169	oveq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
171	167 170	eqtr2d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) )
172		hash0	⊢ ( ♯ ‘ ∅ ) = 0
173	172	oveq2i	⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 )
174	107 111	nn0addcld	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℕ₀ )
175	174	nn0cnd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℂ )
176	175	addridd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) )
177	173 176	eqtr2id	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) )
178	79 144 146 83 165 171 177	splval2	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
179	142 178	eqtrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ) ++ ( ( 𝑓 substr ⟨ 𝑐 , ( ♯ ‘ 𝑓 ) ⟩ ) ++ 𝐵 ) ) )
180	90 105 179	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) )
181	1 2 3 4	efgtf	⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) , 𝑏 ∈ ( 𝐼 × 2_o ) ↦ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 ) )
182	181	simprd	⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 )
183		ffn	⊢ ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) ⟶ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) )
184	72 182 183	3syl	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) )
185		fnovrn	⊢ ( ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2_o ) ) ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
186	184 140 70 185	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
187	180 186	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) )
188	1 2 3 4	efgi2	⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) )
189	72 187 188	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) )
190	1 2 3 4 5 6 7	efgcpbllema	⊢ ( 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ↔ ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ) )
191	67 71 189 190	syl3anbrc	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) )
192		vex	⊢ 𝑎 ∈ V
193		vex	⊢ 𝑓 ∈ V
194	192 193	elec	⊢ ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 𝑎 )
195		breq2	⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑓 𝐿 𝑎 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
196	194 195	bitrid	⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) )
197	191 196	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2_o ) ) ) → ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) )
198	197	rexlimdvva	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2_o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) )
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	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∼ ⊆ 𝐿 )

Metamath Proof Explorer

Theorem efgcpbllemb

Proof