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 ‘ 𝑥 ) } ∈ 𝐸 ) } )