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	bilani	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
51		eliun	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
52	50 51	sylib	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
53		sneq	⊢ ( 𝑢 = 𝑤 → { 𝑢 } = { 𝑤 } )
54		fveq2	⊢ ( 𝑢 = 𝑤 → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ 𝑤 ) )
55	54	oveq2d	⊢ ( 𝑢 = 𝑤 → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
56	53 55	xpeq12d	⊢ ( 𝑢 = 𝑤 → ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) = ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
57	56	eleq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
58	57	cbvrexvw	⊢ ( ∃ 𝑢 ∈ Word 𝐴 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝐴 𝑏 ∈ ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
59	52 58	sylibr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∃ 𝑢 ∈ Word 𝐴 𝑏 ∈ ( { 𝑢 } × ( 0 ... ( ♯ ‘ 𝑢 ) ) ) )
60	48 59	r19.29a	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
61		pfxcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
62	60 61	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
63		swrdcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
64	60 63	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
65	62 64	opelxpd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ∈ ( Word 𝐴 × Word 𝐴 ) )
66	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
67		eliunxp	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
68	66 67	sylib	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
69		opeq1	⊢ ( 𝑢 = 𝑤 → ⟨ 𝑢 , 𝑛 ⟩ = ⟨ 𝑤 , 𝑛 ⟩ )
70	69	eqeq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ↔ 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ) )
71		eleq1w	⊢ ( 𝑢 = 𝑤 → ( 𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴 ) )
72	55	eleq2d	⊢ ( 𝑢 = 𝑤 → ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ↔ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
73	71 72	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ↔ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
74	70 73	anbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) ) )
75	74	exbidv	⊢ ( 𝑢 = 𝑤 → ( ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) ) )
76	75	cbvexvw	⊢ ( ∃ 𝑢 ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) ↔ ∃ 𝑤 ∃ 𝑛 ( 𝑏 = ⟨ 𝑤 , 𝑛 ⟩ ∧ ( 𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ) )
77	68 76	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∃ 𝑢 ∃ 𝑛 ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ∧ ( 𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ) )
78		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 ‘ 𝑏 ) ) )
79		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 ‘ 𝑏 ) ) ⟩ ) )
80	78 79	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 ‘ 𝑏 ) ) ⟩ ) ) )
81		vex	⊢ 𝑢 ∈ V
82		vex	⊢ 𝑛 ∈ V
83	81 82	op1std	⊢ ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ → ( 1^st ‘ 𝑏 ) = 𝑢 )
84	83	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑏 ) = 𝑢 )
85		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑢 ∈ Word 𝐴 )
86	84 85	eqeltrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
87	81 82	op2ndd	⊢ ( 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ → ( 2^nd ‘ 𝑏 ) = 𝑛 )
88	87	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( 2^nd ‘ 𝑏 ) = 𝑛 )
89		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) )
90	84	eqcomd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑢 = ( 1^st ‘ 𝑏 ) )
91	90	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) )
92	91	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 ‘ 𝑏 ) ) ) )
93	89 92	eleqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) ∧ ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) )
94	88 93	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 ‘ 𝑏 ) ) ) )
95		pfxcctswrd	⊢ ( ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑏 ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) ) → ( ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ++ ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ) = ( 1^st ‘ 𝑏 ) )
96	86 94 95	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 ‘ 𝑏 ) )
97	80 96	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 ‘ 𝑎 ) ) )
98	78	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 ‘ 𝑏 ) ) ) )
99		pfxlen	⊢ ( ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑏 ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ) = ( 2^nd ‘ 𝑏 ) )
100	86 94 99	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 ‘ 𝑏 ) )
101	98 100	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 ‘ 𝑎 ) ) )
102	97 101	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 ‘ 𝑎 ) ) ) )
103	102	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 ‘ 𝑎 ) ) ) )
104		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) )
105		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) )
106	104 105	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 ‘ 𝑎 ) ) ) )
107	11	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 )
108	13	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 )
109		pfxccat1	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) prefix ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) = ( 1^st ‘ 𝑎 ) )
110	107 108 109	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) prefix ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) = ( 1^st ‘ 𝑎 ) )
111	106 110	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 1^st ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) )
112	104	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) = ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) )
113	107 108 34	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
114	112 113	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) )
115	105 114	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 ‘ 𝑎 ) ) ) ⟩ )
116	104 115	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 ‘ 𝑎 ) ) ) ⟩ ) )
117		swrdccat2	⊢ ( ( ( 1^st ‘ 𝑎 ) ∈ Word 𝐴 ∧ ( 2^nd ‘ 𝑎 ) ∈ Word 𝐴 ) → ( ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) substr ⟨ ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) , ( ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) + ( ♯ ‘ ( 2^nd ‘ 𝑎 ) ) ) ⟩ ) = ( 2^nd ‘ 𝑎 ) )
118	107 108 117	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 ‘ 𝑎 ) )
119	116 118	eqtr2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 = ⟨ 𝑢 , 𝑛 ⟩ ) ∧ 𝑢 ∈ Word 𝐴 ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ) ∧ ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) → ( 2^nd ‘ 𝑎 ) = ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) )
120	111 119	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 ‘ 𝑏 ) ) ⟩ ) ) )
121	120	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 ‘ 𝑏 ) ) ⟩ ) ) )
122	103 121	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 ‘ 𝑎 ) ) ) ) )
123	122	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 ‘ 𝑎 ) ) ) ) )
124	123	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 ‘ 𝑎 ) ) ) ) ) )
125	124	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 ‘ 𝑎 ) ) ) ) ) )
126	125	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 ‘ 𝑎 ) ) ) ) ) )
127	126	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 ‘ 𝑎 ) ) ) ) )
128	77 127	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 ‘ 𝑎 ) ) ) ) )
129		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 ‘ 𝑏 ) ) ⟩ ) ) ) )
130	129	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 ‘ 𝑏 ) ) ⟩ ) ) ) )
131		snssi	⊢ ( 𝑤 ∈ Word 𝐴 → { 𝑤 } ⊆ Word 𝐴 )
132	131	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑤 ∈ Word 𝐴 ) → { 𝑤 } ⊆ Word 𝐴 )
133		fz0ssnn0	⊢ ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ℕ₀
134		xpss12	⊢ ( ( { 𝑤 } ⊆ Word 𝐴 ∧ ( 0 ... ( ♯ ‘ 𝑤 ) ) ⊆ ℕ₀ ) → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
135	132 133 134	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑤 ∈ Word 𝐴 ) → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
136	135	iunssd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
137	136	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ⊆ ( Word 𝐴 × ℕ₀ ) )
138	137 66	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → 𝑏 ∈ ( Word 𝐴 × ℕ₀ ) )
139		eqop	⊢ ( 𝑏 ∈ ( Word 𝐴 × ℕ₀ ) → ( 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
140	138 139	syl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ↔ ( ( 1^st ‘ 𝑏 ) = ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) ∧ ( 2^nd ‘ 𝑏 ) = ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ) ) )
141	128 130 140	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
142	141	an32s	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ) ∧ 𝑏 ∈ 𝑈 ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
143	142	anasss	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ↔ 𝑏 = ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
144	2 41 65 143	f1ocnv2d	⊢ ( 𝜑 → ( 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 ∧ ^◡ 𝐹 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) )
145	144	simpld	⊢ ( 𝜑 → 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 )
146	144	simprd	⊢ ( 𝜑 → ^◡ 𝐹 = ( 𝑏 ∈ 𝑈 ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
147	146 3	eqtr4di	⊢ ( 𝜑 → ^◡ 𝐹 = 𝐺 )
148	145 147	jca	⊢ ( 𝜑 → ( 𝐹 : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ 𝑈 ∧ ^◡ 𝐹 = 𝐺 ) )

Metamath Proof Explorer

Theorem gsumwrd2dccatlem

Proof