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
|- X = ( ( N + 1 ) WWalksN G )
wwlksnextprop.e
|- E = ( Edg ` G )
wwlksnextprop.y
|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
Assertion wwlksnextprop
|- ( N e. NN0 -> { x e. X | ( x ` 0 ) = P } = { x e. X | E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x
 |-  X = ( ( N + 1 ) WWalksN G )
2 wwlksnextprop.e
 |-  E = ( Edg ` G )
3 wwlksnextprop.y
 |-  Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
4 eqidd
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( x prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) )
5 1 wwlksnextproplem1
 |-  ( ( x e. X /\ N e. NN0 ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
6 5 ancoms
 |-  ( ( N e. NN0 /\ x e. X ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
7 6 adantr
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) )
8 eqeq2
 |-  ( ( x ` 0 ) = P -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) <-> ( ( x prefix ( N + 1 ) ) ` 0 ) = P ) )
9 8 adantl
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( ( ( x prefix ( N + 1 ) ) ` 0 ) = ( x ` 0 ) <-> ( ( x prefix ( N + 1 ) ) ` 0 ) = P ) )
10 7 9 mpbid
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( ( x prefix ( N + 1 ) ) ` 0 ) = P )
11 1 2 wwlksnextproplem2
 |-  ( ( x e. X /\ N e. NN0 ) -> { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E )
12 11 ancoms
 |-  ( ( N e. NN0 /\ x e. X ) -> { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E )
13 12 adantr
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E )
14 simpr
 |-  ( ( N e. NN0 /\ x e. X ) -> x e. X )
15 14 adantr
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> x e. X )
16 simpr
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( x ` 0 ) = P )
17 simpll
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> N e. NN0 )
18 1 2 3 wwlksnextproplem3
 |-  ( ( x e. X /\ ( x ` 0 ) = P /\ N e. NN0 ) -> ( x prefix ( N + 1 ) ) e. Y )
19 15 16 17 18 syl3anc
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( x prefix ( N + 1 ) ) e. Y )
20 eqeq2
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( ( x prefix ( N + 1 ) ) = y <-> ( x prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) ) )
21 fveq1
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( y ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
22 21 eqeq1d
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( ( y ` 0 ) = P <-> ( ( x prefix ( N + 1 ) ) ` 0 ) = P ) )
23 fveq2
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( lastS ` y ) = ( lastS ` ( x prefix ( N + 1 ) ) ) )
24 23 preq1d
 |-  ( y = ( x prefix ( N + 1 ) ) -> { ( lastS ` y ) , ( lastS ` x ) } = { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } )
25 24 eleq1d
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( { ( lastS ` y ) , ( lastS ` x ) } e. E <-> { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E ) )
26 20 22 25 3anbi123d
 |-  ( y = ( x prefix ( N + 1 ) ) -> ( ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) <-> ( ( x prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) /\ ( ( x prefix ( N + 1 ) ) ` 0 ) = P /\ { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E ) ) )
27 26 adantl
 |-  ( ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) /\ y = ( x prefix ( N + 1 ) ) ) -> ( ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) <-> ( ( x prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) /\ ( ( x prefix ( N + 1 ) ) ` 0 ) = P /\ { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E ) ) )
28 19 27 rspcedv
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> ( ( ( x prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) /\ ( ( x prefix ( N + 1 ) ) ` 0 ) = P /\ { ( lastS ` ( x prefix ( N + 1 ) ) ) , ( lastS ` x ) } e. E ) -> E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) ) )
29 4 10 13 28 mp3and
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ ( x ` 0 ) = P ) -> E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) )
30 29 ex
 |-  ( ( N e. NN0 /\ x e. X ) -> ( ( x ` 0 ) = P -> E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) ) )
31 21 eqcoms
 |-  ( ( x prefix ( N + 1 ) ) = y -> ( y ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
32 31 eqeq1d
 |-  ( ( x prefix ( N + 1 ) ) = y -> ( ( y ` 0 ) = P <-> ( ( x prefix ( N + 1 ) ) ` 0 ) = P ) )
33 5 eqcomd
 |-  ( ( x e. X /\ N e. NN0 ) -> ( x ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
34 33 ancoms
 |-  ( ( N e. NN0 /\ x e. X ) -> ( x ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
35 34 adantr
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( x ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) )
36 eqeq2
 |-  ( P = ( ( x prefix ( N + 1 ) ) ` 0 ) -> ( ( x ` 0 ) = P <-> ( x ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) ) )
37 36 eqcoms
 |-  ( ( ( x prefix ( N + 1 ) ) ` 0 ) = P -> ( ( x ` 0 ) = P <-> ( x ` 0 ) = ( ( x prefix ( N + 1 ) ) ` 0 ) ) )
38 35 37 syl5ibr
 |-  ( ( ( x prefix ( N + 1 ) ) ` 0 ) = P -> ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( x ` 0 ) = P ) )
39 32 38 syl6bi
 |-  ( ( x prefix ( N + 1 ) ) = y -> ( ( y ` 0 ) = P -> ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( x ` 0 ) = P ) ) )
40 39 imp
 |-  ( ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( x ` 0 ) = P ) )
41 40 3adant3
 |-  ( ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( x ` 0 ) = P ) )
42 41 com12
 |-  ( ( ( N e. NN0 /\ x e. X ) /\ y e. Y ) -> ( ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x ` 0 ) = P ) )
43 42 rexlimdva
 |-  ( ( N e. NN0 /\ x e. X ) -> ( E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) -> ( x ` 0 ) = P ) )
44 30 43 impbid
 |-  ( ( N e. NN0 /\ x e. X ) -> ( ( x ` 0 ) = P <-> E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) ) )
45 44 rabbidva
 |-  ( N e. NN0 -> { x e. X | ( x ` 0 ) = P } = { x e. X | E. y e. Y ( ( x prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) } )