wrd2ind - Metamath Proof Explorer

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

Theorem wrd2ind 14079

Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.) (Proof shortened by AV, 12-Oct-2022.)

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

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

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

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

Step	Hyp	Ref	Expression
1		lencl 13877	. . . . 5 ⊢ (𝐴 ∈ Word 𝑋 → (♯‘𝐴) ∈ ℕ₀)
2		eqeq2 2833	. . . . . . . . 9 ⊢ (𝑛 = 0 → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = 0))
3	2	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 0 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0)))
4	3	imbi1d 344	. . . . . . 7 ⊢ (𝑛 = 0 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)))
5	4	2ralbidv 3199	. . . . . 6 ⊢ (𝑛 = 0 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)))
6		eqeq2 2833	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = 𝑚))
7	6	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚)))
8	7	imbi1d 344	. . . . . . 7 ⊢ (𝑛 = 𝑚 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑)))
9	8	2ralbidv 3199	. . . . . 6 ⊢ (𝑛 = 𝑚 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑)))
10		eqeq2 2833	. . . . . . . . 9 ⊢ (𝑛 = (𝑚 + 1) → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = (𝑚 + 1)))
11	10	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = (𝑚 + 1) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))))
12	11	imbi1d 344	. . . . . . 7 ⊢ (𝑛 = (𝑚 + 1) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
13	12	2ralbidv 3199	. . . . . 6 ⊢ (𝑛 = (𝑚 + 1) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
14		eqeq2 2833	. . . . . . . . 9 ⊢ (𝑛 = (♯‘𝐴) → ((♯‘𝑥) = 𝑛 ↔ (♯‘𝑥) = (♯‘𝐴)))
15	14	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = (♯‘𝐴) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) ↔ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴))))
16	15	imbi1d 344	. . . . . . 7 ⊢ (𝑛 = (♯‘𝐴) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑)))
17	16	2ralbidv 3199	. . . . . 6 ⊢ (𝑛 = (♯‘𝐴) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑛) → 𝜑) ↔ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑)))
18		eqeq1 2825	. . . . . . . . . . 11 ⊢ ((♯‘𝑥) = 0 → ((♯‘𝑥) = (♯‘𝑤) ↔ 0 = (♯‘𝑤)))
19	18	adantl 484	. . . . . . . . . 10 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → ((♯‘𝑥) = (♯‘𝑤) ↔ 0 = (♯‘𝑤)))
20		eqcom 2828	. . . . . . . . . . . . . 14 ⊢ (0 = (♯‘𝑤) ↔ (♯‘𝑤) = 0)
21		hasheq0 13718	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ Word 𝑌 → ((♯‘𝑤) = 0 ↔ 𝑤 = ∅))
22	20, 21	syl5bb 285	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝑌 → (0 = (♯‘𝑤) ↔ 𝑤 = ∅))
23		hasheq0 13718	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
24		wrd2ind.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝜓
25		wrd2ind.1	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → (𝜑 ↔ 𝜓))
26	24, 25	mpbiri 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ∅ ∧ 𝑤 = ∅) → 𝜑)
27	26	ex 415	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → (𝑤 = ∅ → 𝜑))
28	23, 27	syl6bi 255	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 → (𝑤 = ∅ → 𝜑)))
29	28	com13 88	. . . . . . . . . . . . 13 ⊢ (𝑤 = ∅ → ((♯‘𝑥) = 0 → (𝑥 ∈ Word 𝑋 → 𝜑)))
30	22, 29	syl6bi 255	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ Word 𝑌 → (0 = (♯‘𝑤) → ((♯‘𝑥) = 0 → (𝑥 ∈ Word 𝑋 → 𝜑))))
31	30	com24 95	. . . . . . . . . . 11 ⊢ (𝑤 ∈ Word 𝑌 → (𝑥 ∈ Word 𝑋 → ((♯‘𝑥) = 0 → (0 = (♯‘𝑤) → 𝜑))))
32	31	imp31 420	. . . . . . . . . 10 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → (0 = (♯‘𝑤) → 𝜑))
33	19, 32	sylbid 242	. . . . . . . . 9 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ (♯‘𝑥) = 0) → ((♯‘𝑥) = (♯‘𝑤) → 𝜑))
34	33	ex 415	. . . . . . . 8 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → ((♯‘𝑥) = 0 → ((♯‘𝑥) = (♯‘𝑤) → 𝜑)))
35	34	impcomd 414	. . . . . . 7 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑))
36	35	rgen2 3203	. . . . . 6 ⊢ ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 0) → 𝜑)
37		fveq2 6664	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
38		fveq2 6664	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → (♯‘𝑤) = (♯‘𝑢))
39	37, 38	eqeqan12d 2838	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((♯‘𝑥) = (♯‘𝑤) ↔ (♯‘𝑦) = (♯‘𝑢)))
40		fveqeq2 6673	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = 𝑚 ↔ (♯‘𝑦) = 𝑚))
41	40	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((♯‘𝑥) = 𝑚 ↔ (♯‘𝑦) = 𝑚))
42	39, 41	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) ↔ ((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚)))
43		wrd2ind.2	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → (𝜑 ↔ 𝜒))
44	42, 43	imbi12d 347	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑦 ∧ 𝑤 = 𝑢) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
45	44	ancoms 461	. . . . . . . . 9 ⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
46	45	cbvraldva 3459	. . . . . . . 8 ⊢ (𝑤 = 𝑢 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)))
47	46	cbvralvw 3449	. . . . . . 7 ⊢ (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) ↔ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒))
48		pfxcl 14033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝑌 → (𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌)
49	48	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌)
50	49	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌)
51		simprll 777	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌)
52		eqeq1 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) = (♯‘𝑤) ↔ (𝑚 + 1) = (♯‘𝑤)))
53		nn0p1nn 11930	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ)
54		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑤) = (𝑚 + 1) → ((♯‘𝑤) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
55	54	eqcoms 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) = (♯‘𝑤) → ((♯‘𝑤) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
56	53, 55	syl5ibr 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 + 1) = (♯‘𝑤) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
57	52, 56	syl6bi 255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) = (♯‘𝑤) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ)))
58	57	impcom 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
59	58	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ₀ → (♯‘𝑤) ∈ ℕ))
60	59	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) ∈ ℕ)
61	60	nnge1d 11679	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 1 ≤ (♯‘𝑤))
62		wrdlenge1n0 13896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ Word 𝑌 → (𝑤 ≠ ∅ ↔ 1 ≤ (♯‘𝑤)))
63	51, 62	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 ≠ ∅ ↔ 1 ≤ (♯‘𝑤)))
64	61, 63	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅)
65		lswcl 13914	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → (lastS‘𝑤) ∈ 𝑌)
66	51, 64, 65	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (lastS‘𝑤) ∈ 𝑌)
67	50, 66	jca 514	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌))
68		pfxcl 14033	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word 𝑋 → (𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋)
69	68	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋)
70	69	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋)
71		simprlr 778	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋)
72		eleq1 2900	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑥) = (𝑚 + 1) → ((♯‘𝑥) ∈ ℕ ↔ (𝑚 + 1) ∈ ℕ))
73	53, 72	syl5ibr 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑥) = (𝑚 + 1) → (𝑚 ∈ ℕ₀ → (♯‘𝑥) ∈ ℕ))
74	73	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1))) → (𝑚 ∈ ℕ₀ → (♯‘𝑥) ∈ ℕ))
75	74	impcom 410	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) ∈ ℕ)
76	75	nnge1d 11679	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 1 ≤ (♯‘𝑥))
77		wrdlenge1n0 13896	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Word 𝑋 → (𝑥 ≠ ∅ ↔ 1 ≤ (♯‘𝑥)))
78	71, 77	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑥 ≠ ∅ ↔ 1 ≤ (♯‘𝑥)))
79	76, 78	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅)
80		lswcl 13914	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → (lastS‘𝑥) ∈ 𝑋)
81	71, 79, 80	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (lastS‘𝑥) ∈ 𝑋)
82	67, 70, 81	jca32 518	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ₀ ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)))
83	82	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)))
84		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋))
85		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒))
86		simprrl 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) = (♯‘𝑤))
87	86	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) = ((♯‘𝑤) − 1))
88		simprlr 778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Word 𝑋)
89		fzossfz 13050	. . . . . . . . . . . . . . . . . 18 ⊢ (0..^(♯‘𝑥)) ⊆ (0...(♯‘𝑥))
90		simprrr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) = (𝑚 + 1))
91	53	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝑚 + 1) ∈ ℕ)
92	90, 91	eqeltrd 2913	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑥) ∈ ℕ)
93		fzo0end 13123	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑥) ∈ ℕ → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
95	89, 94	sseldi 3964	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥)))
96		pfxlen 14039	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Word 𝑋 ∧ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = ((♯‘𝑥) − 1))
97	88, 95, 96	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = ((♯‘𝑥) − 1))
98		simprll 777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Word 𝑌)
99		oveq1 7157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑤) = (♯‘𝑥) → ((♯‘𝑤) − 1) = ((♯‘𝑥) − 1))
100		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑤) = (♯‘𝑥) → (0...(♯‘𝑤)) = (0...(♯‘𝑥)))
101	99, 100	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑤) = (♯‘𝑥) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
102	101	eqcoms 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑥) = (♯‘𝑤) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
103	102	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
104	103	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)) ↔ ((♯‘𝑥) − 1) ∈ (0...(♯‘𝑥))))
105	95, 104	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤)))
106		pfxlen 14039	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Word 𝑌 ∧ ((♯‘𝑤) − 1) ∈ (0...(♯‘𝑤))) → (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) = ((♯‘𝑤) − 1))
107	98, 105, 106	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) = ((♯‘𝑤) − 1))
108	87, 97, 107	3eqtr4d 2866	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))
109	90	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) − 1) = ((𝑚 + 1) − 1))
110		nn0cn 11901	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
111	110	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑚 ∈ ℂ)
112		ax-1cn 10589	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
113		pncan 10886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
114	111, 112, 113	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((𝑚 + 1) − 1) = 𝑚)
115	97, 109, 114	3eqtrd 2860	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚)
116	108, 115	jca 514	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚))
117	69	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) → (𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋)
118		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → (♯‘𝑦) = (♯‘(𝑥 prefix ((♯‘𝑥) − 1))))
119		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → (♯‘𝑢) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))
120	118, 119	eqeqan12d 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))))
121	120	expcom 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))))
122	121	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) → (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))))
123	122	imp 409	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))))
124		fveqeq2 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ((♯‘𝑦) = 𝑚 ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚))
125	124	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → ((♯‘𝑦) = 𝑚 ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚))
126	123, 125	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → (((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) ↔ ((♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚)))
127		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
128		vex 3497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
129	127, 128, 43	sbc2ie 3849	. . . . . . . . . . . . . . . . . . . 20 ⊢ ([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ 𝜒)
130	129	bicomi 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑)
131	130	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → (𝜒 ↔ [𝑦 / 𝑥][𝑢 / 𝑤]𝜑))
132		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)))
133	132	sbceq1d 3776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → ([𝑦 / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][𝑢 / 𝑤]𝜑))
134		dfsbcq 3773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ([𝑢 / 𝑤]𝜑 ↔ [(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
135	134	sbcbidv 3826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
136	135	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) → ([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
137	136	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → ([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][𝑢 / 𝑤]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
138	131, 133, 137	3bitrd 307	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → (𝜒 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
139	126, 138	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) ∧ 𝑦 = (𝑥 prefix ((♯‘𝑥) − 1))) → ((((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) ↔ (((♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚) → [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑)))
140	117, 139	rspcdv 3614	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ 𝑢 = (𝑤 prefix ((♯‘𝑤) − 1))) → (∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → (((♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚) → [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑)))
141	49, 140	rspcimdv 3612	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → (∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → (((♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = 𝑚) → [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑)))
142	84, 85, 116, 141	syl3c 66	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑)
143	142, 108	jca 514	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))))
144		dfsbcq 3773	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤][𝑦 / 𝑥]𝜑))
145		sbccom 3853	. . . . . . . . . . . . . . . 16 ⊢ ([(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑)
146	144, 145	syl6bb 289	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
147	119	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ((♯‘𝑦) = (♯‘𝑢) ↔ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))))
148	146, 147	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) ↔ ([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))))
149		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → (𝑢 ++ ⟨“𝑠”⟩) = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩))
150	149	sbceq1d 3776	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ([(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
151	148, 150	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑤 prefix ((♯‘𝑤) − 1)) → ((([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
152		s1eq 13948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (lastS‘𝑤) → ⟨“𝑠”⟩ = ⟨“(lastS‘𝑤)”⟩)
153	152	oveq2d 7166	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (lastS‘𝑤) → ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩))
154	153	sbceq1d 3776	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (lastS‘𝑤) → ([((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
155	154	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
156		sbccom 3853	. . . . . . . . . . . . . . . 16 ⊢ ([((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)
157	156	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (lastS‘𝑤) → ([((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
158	157	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
159	155, 158	bitrd 281	. . . . . . . . . . . . 13 ⊢ (𝑠 = (lastS‘𝑤) → ((([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑) ↔ (([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
160		dfsbcq 3773	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑))
161		fveqeq2 6673	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ((♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))) ↔ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))))
162	160, 161	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → (([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) ↔ ([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1))))))
163		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → (𝑦 ++ ⟨“𝑧”⟩) = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩))
164	163	sbceq1d 3776	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ([(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
165	162, 164	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 1)) → ((([𝑦 / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘𝑦) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [(𝑦 ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑) ↔ (([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
166		s1eq 13948	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (lastS‘𝑥) → ⟨“𝑧”⟩ = ⟨“(lastS‘𝑥)”⟩)
167	166	oveq2d 7166	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (lastS‘𝑥) → ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩) = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩))
168	167	sbceq1d 3776	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (lastS‘𝑥) → ([((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
169	168	imbi2d 343	. . . . . . . . . . . . 13 ⊢ (𝑧 = (lastS‘𝑥) → ((([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“𝑧”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑) ↔ (([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)))
170		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋))
171		simpll 765	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌))
172		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (♯‘𝑦) = (♯‘𝑢))
173		wrd2ind.7	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃))
174	170, 171, 172, 173	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → (𝜒 → 𝜃))
175	43	ancoms 461	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = 𝑢 ∧ 𝑥 = 𝑦) → (𝜑 ↔ 𝜒))
176	128, 127, 175	sbc2ie 3849	. . . . . . . . . . . . . . . 16 ⊢ ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ↔ 𝜒)
177		ovex 7183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ++ ⟨“𝑠”⟩) ∈ V
178		ovex 7183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ++ ⟨“𝑧”⟩) ∈ V
179		wrd2ind.3	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑦 ++ ⟨“𝑧”⟩) ∧ 𝑤 = (𝑢 ++ ⟨“𝑠”⟩)) → (𝜑 ↔ 𝜃))
180	179	ancoms 461	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = (𝑢 ++ ⟨“𝑠”⟩) ∧ 𝑥 = (𝑦 ++ ⟨“𝑧”⟩)) → (𝜑 ↔ 𝜃))
181	177, 178, 180	sbc2ie 3849	. . . . . . . . . . . . . . . 16 ⊢ ([(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑 ↔ 𝜃)
182	174, 176, 181	3imtr4g 298	. . . . . . . . . . . . . . 15 ⊢ ((((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) ∧ (♯‘𝑦) = (♯‘𝑢)) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
183	182	ex 415	. . . . . . . . . . . . . 14 ⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((♯‘𝑦) = (♯‘𝑢) → ([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑)))
184	183	impcomd 414	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ Word 𝑌 ∧ 𝑠 ∈ 𝑌) ∧ (𝑦 ∈ Word 𝑋 ∧ 𝑧 ∈ 𝑋)) → (([𝑢 / 𝑤][𝑦 / 𝑥]𝜑 ∧ (♯‘𝑦) = (♯‘𝑢)) → [(𝑢 ++ ⟨“𝑠”⟩) / 𝑤][(𝑦 ++ ⟨“𝑧”⟩) / 𝑥]𝜑))
185	151, 159, 165, 169, 184	vtocl4ga 3579	. . . . . . . . . . . 12 ⊢ ((((𝑤 prefix ((♯‘𝑤) − 1)) ∈ Word 𝑌 ∧ (lastS‘𝑤) ∈ 𝑌) ∧ ((𝑥 prefix ((♯‘𝑥) − 1)) ∈ Word 𝑋 ∧ (lastS‘𝑥) ∈ 𝑋)) → (([(𝑥 prefix ((♯‘𝑥) − 1)) / 𝑥][(𝑤 prefix ((♯‘𝑤) − 1)) / 𝑤]𝜑 ∧ (♯‘(𝑥 prefix ((♯‘𝑥) − 1))) = (♯‘(𝑤 prefix ((♯‘𝑤) − 1)))) → [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
186	83, 143, 185	sylc 65	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑)
187		eqtr2 2842	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → (♯‘𝑤) = (𝑚 + 1))
188	187	ad2antll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) = (𝑚 + 1))
189	188, 91	eqeltrd 2913	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (♯‘𝑤) ∈ ℕ)
190		wrdfin 13876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝑌 → 𝑤 ∈ Fin)
191	190	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑤 ∈ Fin)
192	191	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ∈ Fin)
193		hashnncl 13721	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ Fin → ((♯‘𝑤) ∈ ℕ ↔ 𝑤 ≠ ∅))
194	192, 193	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑤) ∈ ℕ ↔ 𝑤 ≠ ∅))
195	189, 194	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 ≠ ∅)
196		pfxlswccat 14069	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) = 𝑤)
197	196	eqcomd 2827	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑤 ≠ ∅) → 𝑤 = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩))
198	98, 195, 197	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑤 = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩))
199		wrdfin 13876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Word 𝑋 → 𝑥 ∈ Fin)
200	199	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) → 𝑥 ∈ Fin)
201	200	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ∈ Fin)
202		hashnncl 13721	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ Fin → ((♯‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
203	201, 202	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → ((♯‘𝑥) ∈ ℕ ↔ 𝑥 ≠ ∅))
204	92, 203	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 ≠ ∅)
205		pfxlswccat 14069	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) = 𝑥)
206	205	eqcomd 2827	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Word 𝑋 ∧ 𝑥 ≠ ∅) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩))
207	88, 204, 206	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩))
208		sbceq1a 3782	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) → (𝜑 ↔ [((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
209		sbceq1a 3782	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) → ([((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
210	208, 209	sylan9bb 512	. . . . . . . . . . . 12 ⊢ ((𝑤 = ((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) ∧ 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩)) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
211	198, 207, 210	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 1)) ++ ⟨“(lastS‘𝑥)”⟩) / 𝑥][((𝑤 prefix ((♯‘𝑤) − 1)) ++ ⟨“(lastS‘𝑤)”⟩) / 𝑤]𝜑))
212	186, 211	mpbird 259	. . . . . . . . . 10 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ ((𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋) ∧ ((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)))) → 𝜑)
213	212	expr 459	. . . . . . . . 9 ⊢ (((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) ∧ (𝑤 ∈ Word 𝑌 ∧ 𝑥 ∈ Word 𝑋)) → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑))
214	213	ralrimivva 3191	. . . . . . . 8 ⊢ ((𝑚 ∈ ℕ₀ ∧ ∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑))
215	214	ex 415	. . . . . . 7 ⊢ (𝑚 ∈ ℕ₀ → (∀𝑢 ∈ Word 𝑌∀𝑦 ∈ Word 𝑋(((♯‘𝑦) = (♯‘𝑢) ∧ (♯‘𝑦) = 𝑚) → 𝜒) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
216	47, 215	syl5bi 244	. . . . . 6 ⊢ (𝑚 ∈ ℕ₀ → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = 𝑚) → 𝜑) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (𝑚 + 1)) → 𝜑)))
217	5, 9, 13, 17, 36, 216	nn0ind 12071	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℕ₀ → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
218	1, 217	syl 17	. . . 4 ⊢ (𝐴 ∈ Word 𝑋 → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
219	218	3ad2ant1 1129	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → ∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑))
220		fveq2 6664	. . . . . . . . 9 ⊢ (𝑤 = 𝐵 → (♯‘𝑤) = (♯‘𝐵))
221	220	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑤 = 𝐵 → ((♯‘𝑥) = (♯‘𝑤) ↔ (♯‘𝑥) = (♯‘𝐵)))
222	221	anbi1d 631	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) ↔ ((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴))))
223		wrd2ind.5	. . . . . . 7 ⊢ (𝑤 = 𝐵 → (𝜑 ↔ 𝜌))
224	222, 223	imbi12d 347	. . . . . 6 ⊢ (𝑤 = 𝐵 → ((((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) ↔ (((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
225	224	ralbidv 3197	. . . . 5 ⊢ (𝑤 = 𝐵 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) ↔ ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
226	225	rspcv 3617	. . . 4 ⊢ (𝐵 ∈ Word 𝑌 → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
227	226	3ad2ant2 1130	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑤 ∈ Word 𝑌∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝑤) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜑) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌)))
228	219, 227	mpd 15	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → ∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌))
229		eqidd 2822	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (♯‘𝐴) = (♯‘𝐴))
230		fveqeq2 6673	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ((♯‘𝑥) = (♯‘𝐵) ↔ (♯‘𝐴) = (♯‘𝐵)))
231		fveqeq2 6673	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ((♯‘𝑥) = (♯‘𝐴) ↔ (♯‘𝐴) = (♯‘𝐴)))
232	230, 231	anbi12d 632	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) ↔ ((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴))))
233		wrd2ind.4	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝜌 ↔ 𝜏))
234	232, 233	imbi12d 347	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) ↔ (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → 𝜏)))
235	234	rspcv 3617	. . . . . . 7 ⊢ (𝐴 ∈ Word 𝑋 → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → 𝜏)))
236	235	com23 86	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑋 → (((♯‘𝐴) = (♯‘𝐵) ∧ (♯‘𝐴) = (♯‘𝐴)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → 𝜏)))
237	236	expd 418	. . . . 5 ⊢ (𝐴 ∈ Word 𝑋 → ((♯‘𝐴) = (♯‘𝐵) → ((♯‘𝐴) = (♯‘𝐴) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → 𝜏))))
238	237	com34 91	. . . 4 ⊢ (𝐴 ∈ Word 𝑋 → ((♯‘𝐴) = (♯‘𝐵) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏))))
239	238	imp 409	. . 3 ⊢ ((𝐴 ∈ Word 𝑋 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏)))
240	239	3adant2 1127	. 2 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → (∀𝑥 ∈ Word 𝑋(((♯‘𝑥) = (♯‘𝐵) ∧ (♯‘𝑥) = (♯‘𝐴)) → 𝜌) → ((♯‘𝐴) = (♯‘𝐴) → 𝜏)))
241	228, 229, 240	mp2d 49	1 ⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝜏)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 [wsbc 3771 ∅c0 4290 class class class wbr 5058 ‘cfv 6349 (class class class)co 7150 Fincfn 8503 ℂcc 10529 0cc0 10531 1c1 10532 + caddc 10534 ≤ cle 10670 − cmin 10864 ℕcn 11632 ℕ₀cn0 11891 ...cfz 12886 ..^cfzo 13027 ♯chash 13684 Word cword 13855 lastSclsw 13908 ++ cconcat 13916 ⟨“cs1 13943 prefix cpfx 14026

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-n0 11892 df-xnn0 11962 df-z 11976 df-uz 12238 df-fz 12887 df-fzo 13028 df-hash 13685 df-word 13856 df-lsw 13909 df-concat 13917 df-s1 13944 df-substr 13997 df-pfx 14027

This theorem is referenced by: gsmsymgreq 18554

W3C validator