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 ) } )