wrd2indOLD - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wrd2indOLD		Structured version Visualization version GIF version

Theorem wrd2indOLD 13779

Description: Obsolete proof of wrd2ind 13778 as of 12-Oct-2022. (Contributed by AV, 23-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
wrd2ind.1	⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓))
wrd2ind.2	⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒))
wrd2ind.3	⊢ ((𝑥 = (𝑦 ++ ⟨“𝑧”⟩) ∧ 𝑤 = (𝑢 ++ ⟨“𝑠”⟩)) → (𝜑 ↔ 𝜃))
wrd2ind.4	⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏))
wrd2ind.5	⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌))
wrd2ind.6	⊢ 𝜓
wrd2ind.7	⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃))

**Assertion**
Ref	Expression
wrd2indOLD	⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝜏)

Distinct variable groups: 𝑥,𝑤,𝐴 𝑦,𝑤,𝑧,𝐵,𝑥 𝑢,𝑠,𝑤,𝑥,𝑦,𝑧,𝑋 𝑌,𝑠,𝑢,𝑤,𝑥,𝑦,𝑧 𝜒,𝑤,𝑥 𝜑,𝑠,𝑢,𝑦,𝑧 𝜏,𝑥 𝜃,𝑤,𝑥 𝜌,𝑤 Allowed substitution hints: 𝜑(𝑥,𝑤) 𝜓(𝑥,𝑦,𝑧,𝑤,𝑢,𝑠) 𝜒(𝑦,𝑧,𝑢,𝑠) 𝜃(𝑦,𝑧,𝑢,𝑠) 𝜏(𝑦,𝑧,𝑤,𝑢,𝑠) 𝜌(𝑥,𝑦,𝑧,𝑢,𝑠) 𝐴(𝑦,𝑧,𝑢,𝑠) 𝐵(𝑢,𝑠)

Proof of Theorem wrd2indOLD Dummy variables 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lencl 13553	. . . . 5 ⊢ (𝐴 ∈ Word 𝑋 → (♯‘𝐴) ∈ ℕ₀)
2		eqeq2 2810	. . . . . . . . 9 ⊢ (𝑛 = 0 → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = 0))
3	2	anbi2d 623	. . . . . . . 8 ⊢ (𝑛 = 0 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0)))
4	3	imbi1d 333	. . . . . . 7 ⊢ (𝑛 = 0 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)))
5	4	2ralbidv 3170	. . . . . 6 ⊢ (𝑛 = 0 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)))
6		eqeq2 2810	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = 𝑚))
7	6	anbi2d 623	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚)))
8	7	imbi1d 333	. . . . . . 7 ⊢ (𝑛 = 𝑚 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑)))
9	8	2ralbidv 3170	. . . . . 6 ⊢ (𝑛 = 𝑚 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑)))
10		eqeq2 2810	. . . . . . . . 9 ⊢ (𝑛 = (𝑚 + 1) → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = (𝑚 + 1)))
11	10	anbi2d 623	. . . . . . . 8 ⊢ (𝑛 = (𝑚 + 1) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))))
12	11	imbi1d 333	. . . . . . 7 ⊢ (𝑛 = (𝑚 + 1) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
13	12	2ralbidv 3170	. . . . . 6 ⊢ (𝑛 = (𝑚 + 1) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
14		eqeq2 2810	. . . . . . . . 9 ⊢ (𝑛 = (♯‘𝐴) → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = (♯‘𝐴)))
15	14	anbi2d 623	. . . . . . . 8 ⊢ (𝑛 = (♯‘𝐴) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴))))
16	15	imbi1d 333	. . . . . . 7 ⊢ (𝑛 = (♯‘𝐴) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑)))
17	16	2ralbidv 3170	. . . . . 6 ⊢ (𝑛 = (♯‘𝐴) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑)))
18		eqeq1 2803	. . . . . . . . . . . 12 ⊢ ((♯‘𝑥) = 0 → ((♯‘𝑥) = (♯‘𝑤) ↔ 0 = (♯‘𝑤)))
19	18	adantl 474	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → ((♯‘𝑥) = (♯‘𝑤) ↔ 0 = (♯‘𝑤)))
20		eqcom 2806	. . . . . . . . . . . . . . 15 ⊢ (0 = (♯‘𝑤) ↔ (♯‘𝑤) = 0)
21		hasheq0 13404	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ Word 𝑌 → ((♯‘𝑤) = 0 ↔ 𝑤 = ∅))
22	20, 21	syl5bb 275	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ Word 𝑌 → (0 = (♯‘𝑤) ↔ 𝑤 = ∅))
23		hasheq0 13404	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
24		wrd2ind.6	. . . . . . . . . . . . . . . . . 18 ⊢ 𝜓
25		wrd2ind.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓))
26	24, 25	mpbiri 250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → 𝜑)
27	26	ex 402	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (𝑤 = ∅ → 𝜑))
28	23, 27	syl6bi 245	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 → (𝑤 = ∅ → 𝜑)))
29	28	com13 88	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ((♯‘𝑥) = 0 → (𝑥 ∈ Word 𝑋 → 𝜑)))
30	22, 29	syl6bi 245	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝑌 → (0 = (♯‘𝑤) → ((♯‘𝑥) = 0 → (𝑥 ∈ Word 𝑋 → 𝜑))))
31	30	com24 95	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ Word 𝑌 → (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 → (0 = (♯‘𝑤) → 𝜑))))
32	31	imp31 409	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → (0 = (♯‘𝑤) → 𝜑))
33	19, 32	sylbid 232	. . . . . . . . . 10 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → ((♯‘𝑥) = (♯‘𝑤) → 𝜑))
34	33	ex 402	. . . . . . . . 9 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → ((♯‘𝑥) = 0 → ((♯‘𝑥) = (♯‘𝑤) → 𝜑)))
35	34	com23 86	. . . . . . . 8 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → ((♯‘𝑥) = (♯‘𝑤) → ((♯‘𝑥) = 0 → 𝜑)))
36	35	impd 399	. . . . . . 7 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑))
37	36	rgen2 3156	. . . . . 6 ⊢ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)
38		fveq2 6411	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
39		fveq2 6411	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → (♯‘𝑤) = (♯‘𝑢))
40	38, 39	eqeqan12d 2815	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((♯‘𝑥) = (♯‘𝑤) ↔ (♯‘𝑦) = (♯‘𝑢)))
41		fveqeq2 6420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = 𝑚 ↔ (♯‘𝑦) = 𝑚))
42	41	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((♯‘𝑥) = 𝑚 ↔ (♯‘𝑦) = 𝑚))
43	40, 42	anbi12d 625	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) ↔ ((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚)))
44		wrd2ind.2	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒))
45	43, 44	imbi12d 336	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
46	45	ancoms 451	. . . . . . . . 9 ⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
47	46	cbvraldva 3360	. . . . . . . 8 ⊢ (𝑤 = 𝑢 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
48	47	cbvralv 3354	. . . . . . 7 ⊢ (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒))
49		swrdcl 13669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝑌 → (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌)
50	49	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌)
51	50	ad2antrl 720	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌)
52		simprll 798	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌)
53		eqeq1 2803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) = (♯‘𝑤) ↔ (𝑚 + 1) = (♯‘𝑤)))
54		nn0p1nn 11621	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
55		eleq1 2866	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑤) = (𝑚 + 1) → ((♯‘𝑤) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
56	55	eqcoms 2807	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) = (♯‘𝑤) → ((♯‘𝑤) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
57	54, 56	syl5ibr 238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 + 1) = (♯‘𝑤) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
58	53, 57	syl6bi 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) = (♯‘𝑤) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ)))
59	58	impcom 397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
60	59	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
61	60	impcom 397	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) ∈ ℕ)
62	61	nnge1d 11361	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 1 ≤ (♯‘𝑤))
63		wrdlenge1n0 13570	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ Word 𝑌 → (𝑤 ≠ ∅ ↔ 1 ≤ (♯‘𝑤)))
64	52, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 ≠ ∅ ↔ 1 ≤ (♯‘𝑤)))
65	62, 64	mpbird 249	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅)
66		lswcl 13588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → (lastS‘𝑤) ∈ 𝑌)
67	52, 65, 66	syl2anc 580	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (lastS‘𝑤) ∈ 𝑌)
68	51, 67	jca 508	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌))
69		swrdcl 13669	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word 𝑋 → (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋)
70	69	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋)
71	70	ad2antrl 720	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋)
72		simprlr 799	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋)
73		eleq1 2866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
74	54, 73	syl5ibr 238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑥) = (𝑚 + 1) → (𝑚 ∈ ℕ₀ → (♯‘𝑥) ∈ ℕ))
75	74	ad2antll 721	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ₀ → (♯‘𝑥) ∈ ℕ))
76	75	impcom 397	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) ∈ ℕ)
77	76	nnge1d 11361	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 1 ≤ (♯‘𝑥))
78		wrdlenge1n0 13570	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Word 𝑋 → (𝑥 ≠ ∅ ↔ 1 ≤ (♯‘𝑥)))
79	72, 78	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑥 ≠ ∅ ↔ 1 ≤ (♯‘𝑥)))
80	77, 79	mpbird 249	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅)
81		lswcl 13588	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → (lastS‘𝑥) ∈ 𝑋)
82	72, 80, 81	syl2anc 580	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (lastS‘𝑥) ∈ 𝑋)
83	68, 71, 82	jca32 512	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)))
84	83	adantlr 707	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)))
85		simprl 788	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋))
86		simplr 786	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒))
87		simprrl 800	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) = (♯‘𝑤))
88	87	oveq1d 6893	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) = ((♯‘𝑤) − 1))
89		simprlr 799	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋)
90		fzossfz 12743	. . . . . . . . . . . . . . . . . 18 ⊢ (0..^(♯‘𝑥)) ⊆ (0...(♯‘𝑥))
91		simprrr 801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) = (𝑚 + 1))
92	54	ad2antrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑚 + 1) ∈ ℕ)
93	91, 92	eqeltrd 2878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) ∈ ℕ)
94		fzo0end 12815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑥) ∈ ℕ → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
95	93, 94	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
96	90, 95	sseldi 3796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥)))
97		swrd0lenOLD 13672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Word 𝑋 ∧ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))) → (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = ((♯‘𝑥) − 1))
98	89, 96, 97	syl2anc 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = ((♯‘𝑥) − 1))
99		simprll 798	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌)
100		oveq1 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑤) = (♯‘𝑥) → ((♯‘𝑤) − 1) = ((♯‘𝑥) − 1))
101		oveq2 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑤) = (♯‘𝑥) → (0...(♯‘𝑤)) = (0...(♯‘𝑥)))
102	100, 101	eleq12d 2872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑤) = (♯‘𝑥) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
103	102	eqcoms 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑥) = (♯‘𝑤) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
104	103	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
105	104	ad2antll 721	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
106	96, 105	mpbird 249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)))
107		swrd0lenOLD 13672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Word 𝑌 ∧ ((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤))) → (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) = ((♯‘𝑤) − 1))
108	99, 106, 107	syl2anc 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) = ((♯‘𝑤) − 1))
109	88, 98, 108	3eqtr4d 2843	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))
110	91	oveq1d 6893	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) = ((𝑚 + 1) − 1))
111		nn0cn 11591	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
112	111	ad2antrr 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑚 ∈ ℂ)
113		ax-1cn 10282	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
114		pncan 10578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
115	112, 113, 114	sylancl 581	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((𝑚 + 1) − 1) = 𝑚)
116	98, 110, 115	3eqtrd 2837	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚)
117	109, 116	jca 508	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚))
118	70	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) → (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋)
119		fveq2 6411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → (♯‘𝑦) = (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)))
120		fveq2 6411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → (♯‘𝑢) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))
121	119, 120	eqeqan12d 2815	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))))
122	121	expcom 403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))))
123	122	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) → (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))))
124	123	imp 396	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))))
125		fveqeq2 6420	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ((♯‘𝑦) = 𝑚 ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚))
126	125	adantl 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → ((♯‘𝑦) = 𝑚 ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚))
127	124, 126	anbi12d 625	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) ↔ ((♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚)))
128		vex 3388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
129		vex 3388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
130	128, 129, 44	sbc2ie 3701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ 𝜒)
131	130	bicomi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑)
132	131	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑))
133		simpr 478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩))
134	133	sbceq1d 3638	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → ([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][𝑢 / 𝑤]𝜑))
135		dfsbcq 3635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ([𝑢 / 𝑤]𝜑 ↔ [(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
136	135	sbcbidv 3688	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
137	136	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) → ([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
138	137	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → ([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
139	132, 134, 138	3bitrd 297	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → (𝜒 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
140	127, 139	imbi12d 336	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ 𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) → ((((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) ↔ (((♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚) → [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑)))
141	118, 140	rspcdv 3500	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) → (∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → (((♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚) → [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑)))
142	50, 141	rspcimdv 3498	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → (((♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = 𝑚) → [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑)))
143	85, 86, 117, 142	syl3c 66	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑)
144	143, 109	jca 508	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))))
145		dfsbcq 3635	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤][𝑦 / 𝑥]𝜑))
146		sbccom 3705	. . . . . . . . . . . . . . . 16 ⊢ ([(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑)
147	145, 146	syl6bb 279	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
148	120	eqeq2d 2809	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))))
149	147, 148	anbi12d 625	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) ↔ ([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))))
150		oveq1 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → (𝑢 ++ ⟨“𝑠”⟩) = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩))
151	150	sbceq1d 3638	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ([(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
152	149, 151	imbi12d 336	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) → ((([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
153		s1eq 13620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (lastS‘𝑤) → ⟨“𝑠”⟩ = ⟨“(lastS‘𝑤)”⟩)
154	153	oveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (lastS‘𝑤) → ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩))
155	154	sbceq1d 3638	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (lastS‘𝑤) → ([((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
156	155	imbi2d 332	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
157		sbccom 3705	. . . . . . . . . . . . . . . 16 ⊢ ([((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)
158	157	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (lastS‘𝑤) → ([((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
159	158	imbi2d 332	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
160	156, 159	bitrd 271	. . . . . . . . . . . . 13 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
161		dfsbcq 3635	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ↔ [(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑))
162		fveqeq2 6420	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ((♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)) ↔ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))))
163	161, 162	anbi12d 625	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → (([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) ↔ ([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩)))))
164		oveq1 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → (𝑦 ++ ⟨“𝑧”⟩) = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩))
165	164	sbceq1d 3638	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ([(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
166	163, 165	imbi12d 336	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) → ((([𝑦 / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑) ↔ (([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
167		s1eq 13620	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (lastS‘𝑥) → ⟨“𝑧”⟩ = ⟨“(lastS‘𝑥)”⟩)
168	167	oveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (lastS‘𝑥) → ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩))
169	168	sbceq1d 3638	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (lastS‘𝑥) → ([((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
170	169	imbi2d 332	. . . . . . . . . . . . 13 ⊢ (𝑧 = (lastS‘𝑥) → ((([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑) ↔ (([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
171		simplr 786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋))
172		simpll 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌))
173		simpr 478	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (♯‘𝑦) = (♯‘𝑢))
174		wrd2ind.7	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃))
175	171, 172, 173, 174	syl3anc 1491	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃))
176	44	ancoms 451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒))
177	129, 128, 176	sbc2ie 3701	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ 𝜒)
178		ovex 6910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ++ ⟨“𝑠”⟩) ∈ V
179		ovex 6910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ++ ⟨“𝑧”⟩) ∈ V
180		wrd2ind.3	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = (𝑦 ++ ⟨“𝑧”⟩) ∧ 𝑤 = (𝑢 ++ ⟨“𝑠”⟩)) → (𝜑 ↔ 𝜃))
181	180	ancoms 451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = (𝑢 ++ ⟨“𝑠”⟩) ∧ 𝑥 = (𝑦 ++ ⟨“𝑧”⟩)) → (𝜑 ↔ 𝜃))
182	178, 179, 181	sbc2ie 3701	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ 𝜃)
183	175, 177, 182	3imtr4g 288	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
184	183	ex 402	. . . . . . . . . . . . . . 15 ⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((♯‘𝑦) = (♯‘𝑢) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
185	184	com23 86	. . . . . . . . . . . . . 14 ⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → ((♯‘𝑦) = (♯‘𝑢) → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
186	185	impd 399	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
187	152, 160, 166, 170, 186	vtocl4ga 3466	. . . . . . . . . . . 12 ⊢ ((((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)) → (([(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) / 𝑥][(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) / 𝑤]𝜑 ∧ (♯‘(𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩)) = (♯‘(𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩))) → [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
188	84, 144, 187	sylc 65	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)
189		eqtr2 2819	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (♯‘𝑤) = (𝑚 + 1))
190	189	ad2antll 721	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) = (𝑚 + 1))
191	190, 92	eqeltrd 2878	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) ∈ ℕ)
192		wrdfin 13552	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝑌 → 𝑤 ∈ Fin)
193	192	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑤 ∈ Fin)
194	193	ad2antrl 720	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Fin)
195		hashnncl 13407	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ Fin → ((♯‘𝑤) ∈ ℕ ↔ 𝑤 ≠ ∅))
196	194, 195	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑤) ∈ ℕ ↔ 𝑤 ≠ ∅))
197	191, 196	mpbid 224	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅)
198		swrdccatwrdOLD 13764	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) = 𝑤)
199	198	eqcomd 2805	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → 𝑤 = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩))
200	99, 197, 199	syl2anc 580	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩))
201		wrdfin 13552	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Word 𝑋 → 𝑥 ∈ Fin)
202	201	adantl 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑥 ∈ Fin)
203	202	ad2antrl 720	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Fin)
204		hashnncl 13407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Fin → ((♯‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
205	203, 204	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
206	93, 205	mpbid 224	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅)
207		swrdccatwrdOLD 13764	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) = 𝑥)
208	207	eqcomd 2805	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → 𝑥 = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩))
209	89, 206, 208	syl2anc 580	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩))
210		sbceq1a 3644	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) → (𝜑 ↔ [((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
211		sbceq1a 3644	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) → ([((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
212	210, 211	sylan9bb 506	. . . . . . . . . . . 12 ⊢ ((𝑤 = ((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) ∧ 𝑥 = ((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩)) → (𝜑 ↔ [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
213	200, 209, 212	syl2anc 580	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝜑 ↔ [((𝑥 substr ⟨0, ((♯‘𝑥) − 1)⟩) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 substr ⟨0, ((♯‘𝑤) − 1)⟩) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
214	188, 213	mpbird 249	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝜑)
215	214	expr 449	. . . . . . . . 9 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋)) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑))
216	215	ralrimivva 3152	. . . . . . . 8 ⊢ ((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑))
217	216	ex 402	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
218	48, 217	syl5bi 234	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
219	5, 9, 13, 17, 37, 218	nn0ind 11762	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℕ₀ → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
220	1, 219	syl 17	. . . 4 ⊢ (𝐴 ∈ Word 𝑋 → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
221	220	3ad2ant1 1164	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
222		fveq2 6411	. . . . . . . . 9 ⊢ (𝑤 = 𝐵 → (♯‘𝑤) = (♯‘𝐵))
223	222	eqeq2d 2809	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → ((♯‘𝑥) = (♯‘𝑤) ↔ (♯‘𝑥) = (♯‘𝐵)))
224	223	anbi1d 624	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) ↔ ((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴))))
225		wrd2ind.5	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌))
226	224, 225	imbi12d 336	. . . . . 6 ⊢ (𝑤 = 𝐵 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
227	226	ralbidv 3167	. . . . 5 ⊢ (𝑤 = 𝐵 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) ↔ ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
228	227	rspcv 3493	. . . 4 ⊢ (𝐵 ∈ Word 𝑌 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
229	228	3ad2ant2 1165	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
230	221, 229	mpd 15	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌))
231		eqidd 2800	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (♯‘𝐴) = (♯‘𝐴))
232		fveqeq2 6420	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ((♯‘𝑥) = (♯‘𝐵) ↔ (♯‘𝐴) = (♯‘𝐵)))
233		fveqeq2 6420	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ((♯‘𝑥) = (♯‘𝐴) ↔ (♯‘𝐴) = (♯‘𝐴)))
234	232, 233	anbi12d 625	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) ↔ ((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴))))
235		wrd2ind.4	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏))
236	234, 235	imbi12d 336	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) ↔ (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → 𝜏)))
237	236	rspcv 3493	. . . . . . 7 ⊢ (𝐴 ∈ Word 𝑋 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → 𝜏)))
238	237	com23 86	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑋 → (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → 𝜏)))
239	238	expd 405	. . . . 5 ⊢ (𝐴 ∈ Word 𝑋 → ((♯‘𝐴) = (♯‘𝐵) → ((♯‘𝐴) = (♯‘𝐴) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → 𝜏))))
240	239	com34 91	. . . 4 ⊢ (𝐴 ∈ Word 𝑋 → ((♯‘𝐴) = (♯‘𝐵) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏))))
241	240	imp 396	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏)))
242	241	3adant2 1162	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏)))
243	230, 231, 242	mp2d 49	1 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝜏)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ≠ wne 2971 ∀wral 3089 [wsbc 3633 ∅c0 4115 ⟨cop 4374 class class class wbr 4843 ‘cfv 6101 (class class class)co 6878 Fincfn 8195 ℂcc 10222 0cc0 10224 1c1 10225 + caddc 10227 ≤ cle 10364 − cmin 10556 ℕcn 11312 ℕ₀cn0 11580 ...cfz 12580 ..^cfzo 12720 ♯chash 13370 Word cword 13534 lastSclsw 13582 ++ cconcat 13590 ⟨“cs1 13615 substr csubstr 13664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-int 4668 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-pred 5898 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-om 7300 df-1st 7401 df-2nd 7402 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-oadd 7803 df-er 7982 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-card 9051 df-pnf 10365 df-mnf 10366 df-xr 10367 df-ltxr 10368 df-le 10369 df-sub 10558 df-neg 10559 df-nn 11313 df-n0 11581 df-xnn0 11653 df-z 11667 df-uz 11931 df-fz 12581 df-fzo 12721 df-hash 13371 df-word 13535 df-lsw 13583 df-concat 13591 df-s1 13616 df-substr 13665

This theorem is referenced by: (None)

W3C validator