gsumwrd2dccatlem

Description: Lemma for gsumwrd2dccat . Expose a bijection F between (ordered) pairs of words and words with a length of a subword. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumwrd2dccatlem.u	⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) )
	gsumwrd2dccatlem.f	⊢ 𝐹 = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ )
	gsumwrd2dccatlem.g	⊢ 𝐺 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ )
	gsumwrd2dccatlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	gsumwrd2dccatlem	⊢ ( 𝜑 → ( 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 ∧ ^◡ 𝐹 = 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumwrd2dccatlem.u	⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) )
2		gsumwrd2dccatlem.f	⊢ 𝐹 = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ )
3		gsumwrd2dccatlem.g	⊢ 𝐺 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ )
4		gsumwrd2dccatlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		sneq	⊢ ( 𝑤 = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) → { 𝑤 } = { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) } )
6		fveq2	⊢ ( 𝑤 = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) )
7	6	oveq2d	⊢ ( 𝑤 = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ) )
8	5 7	xpeq12d	⊢ ( 𝑤 = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) = ( { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) } × ( 0 ... ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ) ) )
9	8	eleq2d	⊢ ( 𝑤 = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) → ( ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↔ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ ( { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) } × ( 0 ... ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ) ) ) )
10		xp1st	⊢ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) → ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 )
12		xp2nd	⊢ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) → ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 )
14		ccatcl	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ Word 𝐴 )
15	11 13 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ Word 𝐴 )
16		ovex	⊢ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ V
17	16	snid	⊢ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) }
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) } )
19		0zd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 0 ∈ ℤ )
20		lencl	⊢ ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∈ Word 𝐴 → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∈ ℕ₀ )
21	15 20	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∈ ℕ₀ )
22	21	nn0zd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∈ ℤ )
23		lencl	⊢ ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ∈ ℕ₀ )
24	11 23	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ∈ ℕ₀ )
25	24	nn0zd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ∈ ℤ )
26	24	nn0ge0d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 0 ≤ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) )
27		lencl	⊢ ( ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 → ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ∈ ℕ₀ )
28	13 27	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ∈ ℕ₀ )
29	28	nn0ge0d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 0 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) )
30	24	nn0red	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ∈ ℝ )
31	28	nn0red	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ∈ ℝ )
32	30 31	addge01d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 0 ≤ ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ) )
33	29 32	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ≤ ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
34		ccatlen	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
35	11 13 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
36	33 35	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ≤ ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) )
37	19 22 25 26 36	elfzd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ∈ ( 0 ... ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ) )
38	18 37	opelxpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ ( { ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) } × ( 0 ... ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ) ) )
39	9 15 38	rspcedvdw	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∃ 𝑤 ∈ Word 𝐴 ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
40	39	eliund	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
41	40 1	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ∈ 𝑈 )
42		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) )
43		xp1st	⊢ ( 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) → ( 1^st ‘ 𝑏 ) ∈ { 𝑢 } )
44		elsni	⊢ ( ( 1^st ‘ 𝑏 ) ∈ { 𝑢 } → ( 1^st ‘ 𝑏 ) = 𝑢 )
45	42 43 44	3syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( 1^st ‘ 𝑏 ) = 𝑢 )
46		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → 𝑢 ∈ Word 𝐴 )
47	45 46	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
48	47	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
49	1	eleq2i	⊢ ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
50	49	biimpi	⊢ ( 𝑏 ∈ 𝑈 → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
51	50	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
52		eliun	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
53	51 52	sylib	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
54		sneq	⊢ ( 𝑢 = 𝑤 → { 𝑢 } = { 𝑤 } )
55		fveq2	⊢ ( 𝑢 = 𝑤 → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ 𝑤 ) )
56	55	oveq2d	⊢ ( 𝑢 = 𝑤 → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
57	54 56	xpeq12d	⊢ ( 𝑢 = 𝑤 → ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) = ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
58	57	eleq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
59	58	cbvrexvw	⊢ ( ∃ 𝑢 ∈ Word 𝐴 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
60	53 59	sylibr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∃ 𝑢 ∈ Word 𝐴 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) )
61	48 60	r19.29a	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
62		pfxcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
63	61 62	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
64		swrdcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
65	61 64	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
66	63 65	opelxpd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ∈ ( Word 𝐴 × Word 𝐴 ) )
67	51	adantr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
68		eliunxp	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
69	67 68	sylib	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
70		opeq1	⊢ ( 𝑢 = 𝑤 → ⟨ 𝑢 , 𝑛 ⟩ = ⟨ 𝑤 , 𝑛 ⟩ )
71	70	eqeq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ↔ 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ) )
72		eleq1w	⊢ ( 𝑢 = 𝑤 → ( 𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴 ) )
73	56	eleq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ↔ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
74	72 73	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
75	71 74	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) ) )
76	75	exbidv	⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) ) )
77	76	cbvexvw	⊢ ( ∃ 𝑢 ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
78	69 77	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∃ 𝑢 ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) )
79		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) )
80		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) )
81	79 80	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) = ( ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ++ ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) )
82		vex	⊢ 𝑢 ∈ V
83		vex	⊢ 𝑛 ∈ V
84	82 83	op1std	⊢ ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ → ( 1^st ‘ 𝑏 ) = 𝑢 )
85	84	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑏 ) = 𝑢 )
86		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑢 ∈ Word 𝐴 )
87	85 86	eqeltrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
88	82 83	op2ndd	⊢ ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ → ( 2^nd ‘ 𝑏 ) = 𝑛 )
89	88	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 2^nd ‘ 𝑏 ) = 𝑛 )
90		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) )
91	85	eqcomd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑢 = ( 1^st ‘ 𝑏 ) )
92	91	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) )
93	92	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) )
94	90 93	eleqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) )
95	89 94	eqeltrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 2^nd ‘ 𝑏 ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) )
96		pfxcctswrd	⊢ ( ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑏 ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) ) → ( ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ++ ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) = ( 1^st ‘ 𝑏 ) )
97	87 95 96	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ++ ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) = ( 1^st ‘ 𝑏 ) )
98	81 97	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) )
99	79	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) = ( ♯ ‘ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) )
100		pfxlen	⊢ ( ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑏 ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) = ( 2^nd ‘ 𝑏 ) )
101	87 95 100	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) = ( 2^nd ‘ 𝑏 ) )
102	99 101	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) )
103	98 102	jca	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) )
104	103	anasss	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ) → ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) )
105		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) )
106		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) )
107	105 106	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) = ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) prefix ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) )
108	11	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 )
109	13	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 )
110		pfxccat1	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) prefix ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) = ( 1^st ‘ 𝑎 ) )
111	108 109 110	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) prefix ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) = ( 1^st ‘ 𝑎 ) )
112	107 111	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) )
113	105	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) = ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) )
114	108 109 34	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
115	113 114	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
116	106 115	opeq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ = ⟨ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) , ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ⟩ )
117	105 116	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) = ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) substr ⟨ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) , ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ⟩ ) )
118		swrdccat2	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) substr ⟨ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) , ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ⟩ ) = ( 2^nd ‘ 𝑎 ) )
119	108 109 118	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) substr ⟨ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) , ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ⟩ ) = ( 2^nd ‘ 𝑎 ) )
120	117 119	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) )
121	112 120	jca	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) )
122	121	anasss	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) → ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) )
123	104 122	impbida	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
124	123	anasss	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
125	124	expl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) ) )
126	125	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) ) )
127	126	exlimdv	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) ) )
128	127	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
129	78 128	exlimddv	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
130		eqop	⊢ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ) )
131	130	adantl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ ( ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) ) )
132		snssi	⊢ ( 𝑤 ∈ Word 𝐴 → { 𝑤 } ⊆ Word 𝐴 )
133	132	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑤 ∈ Word 𝐴 ) → { 𝑤 } ⊆ Word 𝐴 )
134		fz0ssnn0	⊢ ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ℕ₀
135		xpss12	⊢ ( ( { 𝑤 } ⊆ Word 𝐴 ∧ ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ℕ₀ ) → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
136	133 134 135	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
137	136	iunssd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
138	137	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
139	138 67	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑏 ∈ ( Word 𝐴 × ℕ₀ ) )
140		eqop	⊢ ( 𝑏 ∈ ( Word 𝐴 × ℕ₀ ) → ( 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
141	139 140	syl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
142	129 131 141	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
143	142	an32s	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 ∈ 𝑈 ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
144	143	anasss	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
145	2 41 66 144	f1ocnv2d	⊢ ( 𝜑 → ( 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 ∧ ^◡ 𝐹 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) )
146	145	simpld	⊢ ( 𝜑 → 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 )
147	145	simprd	⊢ ( 𝜑 → ^◡ 𝐹 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
148	147 3	eqtr4di	⊢ ( 𝜑 → ^◡ 𝐹 = 𝐺 )
149	146 148	jca	⊢ ( 𝜑 → ( 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 ∧ ^◡ 𝐹 = 𝐺 ) )

Metamath Proof Explorer

Theorem gsumwrd2dccatlem

Proof