Metamath Proof Explorer

Theorem wwlksnextprop

Description: Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
Assertion wwlksnextprop ( 𝑁 ∈ ℕ0 → { 𝑥 ∈ 𝑋 ∣ ( 𝑥 ‘ 0 ) = 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ 𝑋 = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
2 wwlksnextprop.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 wwlksnextprop.y ⊢ 𝑌 = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
4 eqidd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) )
5 1 wwlksnextproplem1 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
6 5 ancoms ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) )
8 eqeq2 ⊢ ( ( 𝑥 ‘ 0 ) = 𝑃 → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
9 8 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = ( 𝑥 ‘ 0 ) ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
10 7 9 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 )
11 1 2 wwlksnextproplem2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 )
12 11 ancoms ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 )
14 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
15 14 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → 𝑥 ∈ 𝑋 )
16 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( 𝑥 ‘ 0 ) = 𝑃 )
17 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → 𝑁 ∈ ℕ0 )
18 1 2 3 wwlksnextproplem3 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ 𝑌 )
19 15 16 17 18 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( 𝑥 prefix ( 𝑁 + 1 ) ) ∈ 𝑌 )
20 eqeq2 ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ↔ ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
21 fveq1 ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( 𝑦 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
22 21 eqeq1d ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( 𝑦 ‘ 0 ) = 𝑃 ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
23 fveq2 ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( lastS ‘ 𝑦 ) = ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) )
24 23 preq1d ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } = { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } )
25 24 eleq1d ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ↔ { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) )
26 20 22 25 3anbi123d ⊢ ( 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ∧ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
27 26 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) ∧ 𝑦 = ( 𝑥 prefix ( 𝑁 + 1 ) ) ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ∧ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
28 19 27 rspcedv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = ( 𝑥 prefix ( 𝑁 + 1 ) ) ∧ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ ( 𝑥 prefix ( 𝑁 + 1 ) ) ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
29 4 10 13 28 mp3and ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 ‘ 0 ) = 𝑃 ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) )
30 29 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ‘ 0 ) = 𝑃 → ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
31 21 eqcoms ⊢ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( 𝑦 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
32 31 eqeq1d ⊢ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( ( 𝑦 ‘ 0 ) = 𝑃 ↔ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 ) )
33 5 eqcomd ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
34 33 ancoms ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) )
36 eqeq2 ⊢ ( 𝑃 = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) → ( ( 𝑥 ‘ 0 ) = 𝑃 ↔ ( 𝑥 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) ) )
37 36 eqcoms ⊢ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 → ( ( 𝑥 ‘ 0 ) = 𝑃 ↔ ( 𝑥 ‘ 0 ) = ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) ) )
38 35 37 syl5ibr ⊢ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) ‘ 0 ) = 𝑃 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) )
39 32 38 syl6bi ⊢ ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 → ( ( 𝑦 ‘ 0 ) = 𝑃 → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) ) )
40 39 imp ⊢ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) )
41 40 3adant3 ⊢ ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) )
42 41 com12 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) )
43 42 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) → ( 𝑥 ‘ 0 ) = 𝑃 ) )
44 30 43 impbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) ) )
45 44 rabbidva ⊢ ( 𝑁 ∈ ℕ0 → { 𝑥 ∈ 𝑋 ∣ ( 𝑥 ‘ 0 ) = 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑌 ( ( 𝑥 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑥 ) } ∈ 𝐸 ) } )