Metamath Proof Explorer

Theorem wwlksnextfun

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

Ref Expression
Hypotheses wwlksnextbij0.v ⊢ V = Vtx ⁡ G
wwlksnextbij0.e ⊢ E = Edg ⁡ G
wwlksnextbij0.d ⊢ D = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
wwlksnextbij0.r ⊢ R = n ∈ V | lastS ⁡ W n ∈ E
wwlksnextbij0.f ⊢ F = t ∈ D ⟼ lastS ⁡ t
Assertion wwlksnextfun ⊢ N ∈ ℕ 0 → F : D ⟶ R

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ V = Vtx ⁡ G
2 wwlksnextbij0.e ⊢ E = Edg ⁡ G
3 wwlksnextbij0.d ⊢ D = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
4 wwlksnextbij0.r ⊢ R = n ∈ V | lastS ⁡ W n ∈ E
5 wwlksnextbij0.f ⊢ F = t ∈ D ⟼ lastS ⁡ t
6 fveqeq2 ⊢ w = t → w = N + 2 ↔ t = N + 2
7 oveq1 ⊢ w = t → w prefix N + 1 = t prefix N + 1
8 7 eqeq1d ⊢ w = t → w prefix N + 1 = W ↔ t prefix N + 1 = W
9 fveq2 ⊢ w = t → lastS ⁡ w = lastS ⁡ t
10 9 preq2d ⊢ w = t → lastS ⁡ W lastS ⁡ w = lastS ⁡ W lastS ⁡ t
11 10 eleq1d ⊢ w = t → lastS ⁡ W lastS ⁡ w ∈ E ↔ lastS ⁡ W lastS ⁡ t ∈ E
12 6 8 11 3anbi123d ⊢ w = t → w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ↔ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E
13 12 3 elrab2 ⊢ t ∈ D ↔ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E
14 simpll ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → t ∈ Word V
15 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
18 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
19 2pos ⊢ 0 < 2
20 19 a1i ⊢ N ∈ ℕ 0 → 0 < 2
21 15 17 18 20 addgegt0d ⊢ N ∈ ℕ 0 → 0 < N + 2
22 21 ad2antlr ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → 0 < N + 2
23 breq2 ⊢ t = N + 2 → 0 < t ↔ 0 < N + 2
24 23 adantl ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → 0 < t ↔ 0 < N + 2
25 22 24 mpbird ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → 0 < t
26 hashgt0n0 ⊢ t ∈ Word V ∧ 0 < t → t ≠ ∅
27 14 25 26 syl2anc ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → t ≠ ∅
28 14 27 jca ⊢ t ∈ Word V ∧ N ∈ ℕ 0 ∧ t = N + 2 → t ∈ Word V ∧ t ≠ ∅
29 28 expcom ⊢ t = N + 2 → t ∈ Word V ∧ N ∈ ℕ 0 → t ∈ Word V ∧ t ≠ ∅
30 29 3ad2ant1 ⊢ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → t ∈ Word V ∧ N ∈ ℕ 0 → t ∈ Word V ∧ t ≠ ∅
31 30 expd ⊢ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → t ∈ Word V → N ∈ ℕ 0 → t ∈ Word V ∧ t ≠ ∅
32 31 impcom ⊢ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → N ∈ ℕ 0 → t ∈ Word V ∧ t ≠ ∅
33 32 impcom ⊢ N ∈ ℕ 0 ∧ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → t ∈ Word V ∧ t ≠ ∅
34 lswcl ⊢ t ∈ Word V ∧ t ≠ ∅ → lastS ⁡ t ∈ V
35 33 34 syl ⊢ N ∈ ℕ 0 ∧ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → lastS ⁡ t ∈ V
36 simprr3 ⊢ N ∈ ℕ 0 ∧ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → lastS ⁡ W lastS ⁡ t ∈ E
37 35 36 jca ⊢ N ∈ ℕ 0 ∧ t ∈ Word V ∧ t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E → lastS ⁡ t ∈ V ∧ lastS ⁡ W lastS ⁡ t ∈ E
38 13 37 sylan2b ⊢ N ∈ ℕ 0 ∧ t ∈ D → lastS ⁡ t ∈ V ∧ lastS ⁡ W lastS ⁡ t ∈ E
39 preq2 ⊢ n = lastS ⁡ t → lastS ⁡ W n = lastS ⁡ W lastS ⁡ t
40 39 eleq1d ⊢ n = lastS ⁡ t → lastS ⁡ W n ∈ E ↔ lastS ⁡ W lastS ⁡ t ∈ E
41 40 4 elrab2 ⊢ lastS ⁡ t ∈ R ↔ lastS ⁡ t ∈ V ∧ lastS ⁡ W lastS ⁡ t ∈ E
42 38 41 sylibr ⊢ N ∈ ℕ 0 ∧ t ∈ D → lastS ⁡ t ∈ R
43 42 5 fmptd ⊢ N ∈ ℕ 0 → F : D ⟶ R