Metamath Proof Explorer

Theorem wwlksnredwwlkn0

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypothesis wwlksnredwwlkn.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion wwlksnredwwlkn0 ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 1 wwlksnredwwlkn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
3 2 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
4 simpl ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 )
5 4 adantl ⊢ ( ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ∧ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 )
6 fveq1 ⊢ ( 𝑦 = ( 𝑊 prefix ( 𝑁 + 1 ) ) → ( 𝑦 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
7 6 eqcoms ⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( 𝑦 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
8 7 adantr ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) → ( 𝑦 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 1 wwlknp ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) )
11 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
12 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
13 nn0re ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
14 lep1 ⊢ ( ( 𝑁 + 1 ) ∈ ℝ → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
15 12 13 14 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) )
16 peano2nn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 )
17 16 nn0zd ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℤ )
18 fznn ⊢ ( ( ( 𝑁 + 1 ) + 1 ) ∈ ℤ → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) ) )
19 12 17 18 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) ) )
20 11 15 19 mpbir2and ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
21 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) )
22 21 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( ( 𝑁 + 1 ) + 1 ) ) ) )
23 20 22 imbitrrid ⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
24 23 adantl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
25 simpl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
26 24 25 jctild ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
27 26 3adant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝐸 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
28 10 27 syl ⊢ ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) ) )
29 28 impcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
30 29 adantl ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
31 30 adantr ⊢ ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
32 31 adantl ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
33 pfxfv0 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
34 32 33 syl ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
35 simprll ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) → ( 𝑊 ‘ 0 ) = 𝑃 )
36 8 34 35 3eqtrd ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
37 36 ex ⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 ) )
38 37 adantr ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 ) )
39 38 impcom ⊢ ( ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ∧ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
40 simpr ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
41 40 adantl ⊢ ( ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ∧ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) → { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 )
42 5 39 41 3jca ⊢ ( ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) ∧ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) )
43 42 ex ⊢ ( ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
44 43 reximdva ⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑃 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
45 44 ex ⊢ ( ( 𝑊 ‘ 0 ) = 𝑃 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) ) )
46 45 com13 ⊢ ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑃 → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) ) )
47 3 46 mpcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑃 → ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )
48 29 33 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
49 48 eqcomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
50 49 adantl ⊢ ( ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( 𝑊 ‘ 0 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
51 fveq1 ⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑦 ‘ 0 ) )
52 51 adantr ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑦 ‘ 0 ) )
53 52 adantr ⊢ ( ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑦 ‘ 0 ) )
54 simpr ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( 𝑦 ‘ 0 ) = 𝑃 )
55 54 adantr ⊢ ( ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
56 50 53 55 3eqtrd ⊢ ( ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ) → ( 𝑊 ‘ 0 ) = 𝑃 )
57 56 ex ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 ‘ 0 ) = 𝑃 ) )
58 57 3adant3 ⊢ ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( 𝑊 ‘ 0 ) = 𝑃 ) )
59 58 com12 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( 𝑊 ‘ 0 ) = 𝑃 ) )
60 59 rexlimdvw ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) → ( 𝑊 ‘ 0 ) = 𝑃 ) )
61 47 60 impbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑊 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑊 ) } ∈ 𝐸 ) ) )