Metamath Proof Explorer

Theorem clwwlknon

Description: The set of closed walks on vertex X of length N in a graph G as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

Ref Expression
Assertion clwwlknon 
|- ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( v = X -> ( ( w ` 0 ) = v <-> ( w ` 0 ) = X ) )
2 1 rabbidv 
 |-  ( v = X -> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } = { w e. ( n ClWWalksN G ) | ( w ` 0 ) = X } )
3 oveq1 
 |-  ( n = N -> ( n ClWWalksN G ) = ( N ClWWalksN G ) )
4 3 rabeqdv 
 |-  ( n = N -> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = X } = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } )
5 clwwlknonmpo 
 |-  ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
6 ovex 
 |-  ( N ClWWalksN G ) e. _V
7 6 rabex 
 |-  { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } e. _V
8 2 4 5 7 ovmpo 
 |-  ( ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } )
9 5 mpondm0 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( X ( ClWWalksNOn ` G ) N ) = (/) )
10 isclwwlkn 
 |-  ( w e. ( N ClWWalksN G ) <-> ( w e. ( ClWWalks ` G ) /\ ( # ` w ) = N ) )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 11 clwwlkbp 
 |-  ( w e. ( ClWWalks ` G ) -> ( G e. _V /\ w e. Word ( Vtx ` G ) /\ w =/= (/) ) )
13 fstwrdne 
 |-  ( ( w e. Word ( Vtx ` G ) /\ w =/= (/) ) -> ( w ` 0 ) e. ( Vtx ` G ) )
14 13 3adant1 
 |-  ( ( G e. _V /\ w e. Word ( Vtx ` G ) /\ w =/= (/) ) -> ( w ` 0 ) e. ( Vtx ` G ) )
15 12 14 syl 
 |-  ( w e. ( ClWWalks ` G ) -> ( w ` 0 ) e. ( Vtx ` G ) )
16 15 adantr 
 |-  ( ( w e. ( ClWWalks ` G ) /\ ( # ` w ) = N ) -> ( w ` 0 ) e. ( Vtx ` G ) )
17 10 16 sylbi 
 |-  ( w e. ( N ClWWalksN G ) -> ( w ` 0 ) e. ( Vtx ` G ) )
18 17 adantr 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> ( w ` 0 ) e. ( Vtx ` G ) )
19 eleq1 
 |-  ( ( w ` 0 ) = X -> ( ( w ` 0 ) e. ( Vtx ` G ) <-> X e. ( Vtx ` G ) ) )
20 19 adantl 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> ( ( w ` 0 ) e. ( Vtx ` G ) <-> X e. ( Vtx ` G ) ) )
21 18 20 mpbid 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> X e. ( Vtx ` G ) )
22 clwwlknnn 
 |-  ( w e. ( N ClWWalksN G ) -> N e. NN )
23 22 nnnn0d 
 |-  ( w e. ( N ClWWalksN G ) -> N e. NN0 )
24 23 adantr 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> N e. NN0 )
25 21 24 jca 
 |-  ( ( w e. ( N ClWWalksN G ) /\ ( w ` 0 ) = X ) -> ( X e. ( Vtx ` G ) /\ N e. NN0 ) )
26 25 ex 
 |-  ( w e. ( N ClWWalksN G ) -> ( ( w ` 0 ) = X -> ( X e. ( Vtx ` G ) /\ N e. NN0 ) ) )
27 26 con3rr3 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( w e. ( N ClWWalksN G ) -> -. ( w ` 0 ) = X ) )
28 27 ralrimiv 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> A. w e. ( N ClWWalksN G ) -. ( w ` 0 ) = X )
29 rabeq0 
 |-  ( { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } = (/) <-> A. w e. ( N ClWWalksN G ) -. ( w ` 0 ) = X )
30 28 29 sylibr 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } = (/) )
31 9 30 eqtr4d 
 |-  ( -. ( X e. ( Vtx ` G ) /\ N e. NN0 ) -> ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X } )
32 8 31 pm2.61i 
 |-  ( X ( ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }