wwlksnextinj - Metamath Proof Explorer

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

Theorem wwlksnextinj 26794

Description: Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)

**Hypotheses**
Ref	Expression
wwlksnextbij0.v	⊢ 𝑉 = (Vtx‘𝐺)
wwlksnextbij0.e	⊢ 𝐸 = (Edg‘𝐺)
wwlksnextbij0.d	⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}
wwlksnextbij.r	⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}
wwlksnextbij.f	⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))

**Assertion**
Ref	Expression
wwlksnextinj	⊢ (𝑁 ∈ ℕ₀ → 𝐹:𝐷–1-1→𝑅)

Distinct variable groups: 𝑤,𝐺 𝑤,𝑁 𝑤,𝑊 𝑡,𝐷 𝑛,𝐸 𝑤,𝐸 𝑡,𝑁,𝑤 𝑡,𝑅 𝑛,𝑉 𝑤,𝑉 𝑛,𝑊 𝑡,𝑛 Allowed substitution hints: 𝐷(𝑤,𝑛) 𝑅(𝑤,𝑛) 𝐸(𝑡) 𝐹(𝑤,𝑡,𝑛) 𝐺(𝑡,𝑛) 𝑁(𝑛) 𝑉(𝑡) 𝑊(𝑡)

Proof of Theorem wwlksnextinj Dummy variables 𝑑 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wwlksnextbij0.v	. . 3 ⊢ 𝑉 = (Vtx‘𝐺)
2		wwlksnextbij0.e	. . 3 ⊢ 𝐸 = (Edg‘𝐺)
3		wwlksnextbij0.d	. . 3 ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}
4		wwlksnextbij.r	. . 3 ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}
5		wwlksnextbij.f	. . 3 ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))
6	1, 2, 3, 4, 5	wwlksnextfun 26793	. 2 ⊢ (𝑁 ∈ ℕ₀ → 𝐹:𝐷⟶𝑅)
7		fveq2 6191	. . . . . . 7 ⊢ (𝑡 = 𝑑 → ( lastS ‘𝑡) = ( lastS ‘𝑑))
8		fvex 6201	. . . . . . 7 ⊢ ( lastS ‘𝑑) ∈ V
9	7, 5, 8	fvmpt 6282	. . . . . 6 ⊢ (𝑑 ∈ 𝐷 → (𝐹‘𝑑) = ( lastS ‘𝑑))
10		fveq2 6191	. . . . . . 7 ⊢ (𝑡 = 𝑥 → ( lastS ‘𝑡) = ( lastS ‘𝑥))
11		fvex 6201	. . . . . . 7 ⊢ ( lastS ‘𝑥) ∈ V
12	10, 5, 11	fvmpt 6282	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = ( lastS ‘𝑥))
13	9, 12	eqeqan12d 2638	. . . . 5 ⊢ ((𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) → ((𝐹‘𝑑) = (𝐹‘𝑥) ↔ ( lastS ‘𝑑) = ( lastS ‘𝑥)))
14	13	adantl 482	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → ((𝐹‘𝑑) = (𝐹‘𝑥) ↔ ( lastS ‘𝑑) = ( lastS ‘𝑥)))
15		fveq2 6191	. . . . . . . . 9 ⊢ (𝑤 = 𝑑 → (#‘𝑤) = (#‘𝑑))
16	15	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑤 = 𝑑 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑑) = (𝑁 + 2)))
17		oveq1 6657	. . . . . . . . 9 ⊢ (𝑤 = 𝑑 → (𝑤 substr ⟨0, (𝑁 + 1)⟩) = (𝑑 substr ⟨0, (𝑁 + 1)⟩))
18	17	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑤 = 𝑑 → ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ↔ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊))
19		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑤 = 𝑑 → ( lastS ‘𝑤) = ( lastS ‘𝑑))
20	19	preq2d 4275	. . . . . . . . 9 ⊢ (𝑤 = 𝑑 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑑)})
21	20	eleq1d 2686	. . . . . . . 8 ⊢ (𝑤 = 𝑑 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸))
22	16, 18, 21	3anbi123d 1399	. . . . . . 7 ⊢ (𝑤 = 𝑑 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸) ↔ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)))
23	22, 3	elrab2 3366	. . . . . 6 ⊢ (𝑑 ∈ 𝐷 ↔ (𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)))
24		fveq2 6191	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (#‘𝑤) = (#‘𝑥))
25	24	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((#‘𝑤) = (𝑁 + 2) ↔ (#‘𝑥) = (𝑁 + 2)))
26		oveq1 6657	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
27	26	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ↔ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊))
28		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ( lastS ‘𝑤) = ( lastS ‘𝑥))
29	28	preq2d 4275	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → {( lastS ‘𝑊), ( lastS ‘𝑤)} = {( lastS ‘𝑊), ( lastS ‘𝑥)})
30	29	eleq1d 2686	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ({( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))
31	25, 27, 30	3anbi123d 1399	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸) ↔ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)))
32	31, 3	elrab2 3366	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)))
33		eqtr3 2643	. . . . . . . . . . . . . . . . 17 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (#‘𝑥) = (𝑁 + 2)) → (#‘𝑑) = (#‘𝑥))
34	33	expcom 451	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑥) = (𝑁 + 2) → ((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥)))
35	34	3ad2ant1 1082	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸) → ((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥)))
36	35	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → ((#‘𝑑) = (𝑁 + 2) → (#‘𝑑) = (#‘𝑥)))
37	36	com12 32	. . . . . . . . . . . . 13 ⊢ ((#‘𝑑) = (𝑁 + 2) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (#‘𝑑) = (#‘𝑥)))
38	37	3ad2ant1 1082	. . . . . . . . . . . 12 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (#‘𝑑) = (#‘𝑥)))
39	38	adantl 482	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (#‘𝑑) = (#‘𝑥)))
40	39	imp 445	. . . . . . . . . 10 ⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) → (#‘𝑑) = (#‘𝑥))
41	40	adantr 481	. . . . . . . . 9 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → (#‘𝑑) = (#‘𝑥))
42	41	adantr 481	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → (#‘𝑑) = (#‘𝑥))
43		simpr 477	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → ( lastS ‘𝑑) = ( lastS ‘𝑥))
44		eqtr3 2643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → (𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
45		1e2m1 11136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 = (2 − 1)
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ₀ → 1 = (2 − 1))
47	46	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) = (𝑁 + (2 − 1)))
48		nn0cn 11302	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
49		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ₀ → 2 ∈ ℂ)
50		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℂ)
51	48, 49, 50	addsubassd 10412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 2) − 1) = (𝑁 + (2 − 1)))
52	47, 51	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) = ((𝑁 + 2) − 1))
53	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ₀ ∧ (#‘𝑑) = (𝑁 + 2)) → (𝑁 + 1) = ((𝑁 + 2) − 1))
54		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝑑) = (𝑁 + 2) → ((#‘𝑑) − 1) = ((𝑁 + 2) − 1))
55	54	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((#‘𝑑) = (𝑁 + 2) → ((𝑁 + 1) = ((#‘𝑑) − 1) ↔ (𝑁 + 1) = ((𝑁 + 2) − 1)))
56	55	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ₀ ∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑁 + 1) = ((#‘𝑑) − 1) ↔ (𝑁 + 1) = ((𝑁 + 2) − 1)))
57	53, 56	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ ℕ₀ ∧ (#‘𝑑) = (𝑁 + 2)) → (𝑁 + 1) = ((#‘𝑑) − 1))
58		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → ⟨0, (𝑁 + 1)⟩ = ⟨0, ((#‘𝑑) − 1)⟩)
59	58	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → (𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩))
60	58	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → (𝑥 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))
61	59, 60	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 + 1) = ((#‘𝑑) − 1) → ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩) ↔ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))
62	57, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ₀ ∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩) ↔ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))
63	62	biimpd 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℕ₀ ∧ (#‘𝑑) = (𝑁 + 2)) → ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩) → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))
64	63	ex 450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((#‘𝑑) = (𝑁 + 2) → ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩) → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
65	64	com13 88	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩) → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
66	44, 65	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
67	66	ex 450	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → ((𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))))
68	67	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → ((#‘𝑑) = (𝑁 + 2) → ((𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))))
69	68	impcom 446	. . . . . . . . . . . . . . . 16 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → ((𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
70	69	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
71	70	3ad2ant2 1083	. . . . . . . . . . . . . 14 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸) → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
72	71	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
73	72	com12 32	. . . . . . . . . . . 12 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
74	73	3adant3 1081	. . . . . . . . . . 11 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
75	74	adantl 482	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) → ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (𝑁 ∈ ℕ₀ → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
76	75	imp31 448	. . . . . . . . 9 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))
77	76	adantr 481	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))
78		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) → 𝑑 ∈ Word 𝑉)
79		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → 𝑥 ∈ Word 𝑉)
80	78, 79	anim12i 590	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) → (𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉))
81	80	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → (𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉))
82		nn0re 11301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
83		2re 11090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 2 ∈ ℝ)
85		nn0ge0 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 0 ≤ 𝑁)
86		2pos 11112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < 2
87	86	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 0 < 2)
88	82, 84, 85, 87	addgegt0d 10601	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → 0 < (𝑁 + 2))
89	88	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → 0 < (𝑁 + 2))
90		breq2 4657	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝑑) = (𝑁 + 2) → (0 < (#‘𝑑) ↔ 0 < (𝑁 + 2)))
91	90	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → (0 < (#‘𝑑) ↔ 0 < (𝑁 + 2)))
92	89, 91	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → 0 < (#‘𝑑))
93		hashgt0n0 13156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ Word 𝑉 ∧ 0 < (#‘𝑑)) → 𝑑 ≠ ∅)
94	92, 93	sylan2 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀)) → 𝑑 ≠ ∅)
95	94	exp32 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ Word 𝑉 → ((#‘𝑑) = (𝑁 + 2) → (𝑁 ∈ ℕ₀ → 𝑑 ≠ ∅)))
96	95	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑑) = (𝑁 + 2) → (𝑑 ∈ Word 𝑉 → (𝑁 ∈ ℕ₀ → 𝑑 ≠ ∅)))
97	96	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ (((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸) → (𝑑 ∈ Word 𝑉 → (𝑁 ∈ ℕ₀ → 𝑑 ≠ ∅)))
98	97	impcom 446	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) → (𝑁 ∈ ℕ₀ → 𝑑 ≠ ∅))
99	98	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) → (𝑁 ∈ ℕ₀ → 𝑑 ≠ ∅))
100	99	imp 445	. . . . . . . . . . 11 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → 𝑑 ≠ ∅)
101	88	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → 0 < (𝑁 + 2))
102		breq2 4657	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝑥) = (𝑁 + 2) → (0 < (#‘𝑥) ↔ 0 < (𝑁 + 2)))
103	102	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → (0 < (#‘𝑥) ↔ 0 < (𝑁 + 2)))
104	101, 103	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀) → 0 < (#‘𝑥))
105		hashgt0n0 13156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ Word 𝑉 ∧ 0 < (#‘𝑥)) → 𝑥 ≠ ∅)
106	104, 105	sylan2 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑁 ∈ ℕ₀)) → 𝑥 ≠ ∅)
107	106	exp32 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word 𝑉 → ((#‘𝑥) = (𝑁 + 2) → (𝑁 ∈ ℕ₀ → 𝑥 ≠ ∅)))
108	107	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑥) = (𝑁 + 2) → (𝑥 ∈ Word 𝑉 → (𝑁 ∈ ℕ₀ → 𝑥 ≠ ∅)))
109	108	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸) → (𝑥 ∈ Word 𝑉 → (𝑁 ∈ ℕ₀ → 𝑥 ≠ ∅)))
110	109	impcom 446	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸)) → (𝑁 ∈ ℕ₀ → 𝑥 ≠ ∅))
111	110	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) → (𝑁 ∈ ℕ₀ → 𝑥 ≠ ∅))
112	111	imp 445	. . . . . . . . . . 11 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → 𝑥 ≠ ∅)
113	81, 100, 112	jca32 558	. . . . . . . . . 10 ⊢ ((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)))
114	113	adantr 481	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)))
115		simpl 473	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 𝑑 ∈ Word 𝑉)
116	115	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 𝑑 ∈ Word 𝑉)
117		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 𝑥 ∈ Word 𝑉)
118	117	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Word 𝑉)
119		hashneq0 13155	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ Word 𝑉 → (0 < (#‘𝑑) ↔ 𝑑 ≠ ∅))
120	119	biimprd 238	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ Word 𝑉 → (𝑑 ≠ ∅ → 0 < (#‘𝑑)))
121	120	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → (𝑑 ≠ ∅ → 0 < (#‘𝑑)))
122	121	com12 32	. . . . . . . . . . . . 13 ⊢ (𝑑 ≠ ∅ → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 0 < (#‘𝑑)))
123	122	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅) → ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) → 0 < (#‘𝑑)))
124	123	impcom 446	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → 0 < (#‘𝑑))
125		2swrd1eqwrdeq 13454	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉 ∧ 0 < (#‘𝑑)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)))))
126	116, 118, 124, 125	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)))))
127		ancom 466	. . . . . . . . . . . 12 ⊢ (((𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) ↔ (( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))
128	127	anbi2i 730	. . . . . . . . . . 11 ⊢ (((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥))) ↔ ((#‘𝑑) = (#‘𝑥) ∧ (( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
129		3anass 1042	. . . . . . . . . . 11 ⊢ (((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)) ↔ ((#‘𝑑) = (#‘𝑥) ∧ (( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
130	128, 129	bitr4i 267	. . . . . . . . . 10 ⊢ (((#‘𝑑) = (#‘𝑥) ∧ ((𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥))) ↔ ((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩)))
131	126, 130	syl6bb 276	. . . . . . . . 9 ⊢ (((𝑑 ∈ Word 𝑉 ∧ 𝑥 ∈ Word 𝑉) ∧ (𝑑 ≠ ∅ ∧ 𝑥 ≠ ∅)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
132	114, 131	syl 17	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → (𝑑 = 𝑥 ↔ ((#‘𝑑) = (#‘𝑥) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥) ∧ (𝑑 substr ⟨0, ((#‘𝑑) − 1)⟩) = (𝑥 substr ⟨0, ((#‘𝑑) − 1)⟩))))
133	42, 43, 77, 132	mpbir3and 1245	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) ∧ 𝑁 ∈ ℕ₀) ∧ ( lastS ‘𝑑) = ( lastS ‘𝑥)) → 𝑑 = 𝑥)
134	133	exp31 630	. . . . . 6 ⊢ (((𝑑 ∈ Word 𝑉 ∧ ((#‘𝑑) = (𝑁 + 2) ∧ (𝑑 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑑)} ∈ 𝐸)) ∧ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = (𝑁 + 2) ∧ (𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑥)} ∈ 𝐸))) → (𝑁 ∈ ℕ₀ → (( lastS ‘𝑑) = ( lastS ‘𝑥) → 𝑑 = 𝑥)))
135	23, 32, 134	syl2anb 496	. . . . 5 ⊢ ((𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) → (𝑁 ∈ ℕ₀ → (( lastS ‘𝑑) = ( lastS ‘𝑥) → 𝑑 = 𝑥)))
136	135	impcom 446	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → (( lastS ‘𝑑) = ( lastS ‘𝑥) → 𝑑 = 𝑥))
137	14, 136	sylbid 230	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑑 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷)) → ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥))
138	137	ralrimivva 2971	. 2 ⊢ (𝑁 ∈ ℕ₀ → ∀𝑑 ∈ 𝐷 ∀𝑥 ∈ 𝐷 ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥))
139		dff13 6512	. 2 ⊢ (𝐹:𝐷–1-1→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑑 ∈ 𝐷 ∀𝑥 ∈ 𝐷 ((𝐹‘𝑑) = (𝐹‘𝑥) → 𝑑 = 𝑥)))
140	6, 138, 139	sylanbrc 698	1 ⊢ (𝑁 ∈ ℕ₀ → 𝐹:𝐷–1-1→𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 ∅c0 3915 {cpr 4179 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 ⟶wf 5884 –1-1→wf1 5885 ‘cfv 5888 (class class class)co 6650 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 < clt 10074 − cmin 10266 2c2 11070 ℕ₀cn0 11292 #chash 13117 Word cword 13291 lastS clsw 13292 substr csubstr 13295 Vtxcvtx 25874 Edgcedg 25939

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-lsw 13300 df-s1 13302 df-substr 13303

This theorem is referenced by: wwlksnextbij0 26796

W3C validator