Metamath Proof Explorer

Theorem clwwlkn

Description: The set of closed walks of a fixed length N as words over the set of vertices in a graph G . (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlkn 
|- ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N }

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( g = G -> ( ClWWalks ` g ) = ( ClWWalks ` G ) )
2 1 adantl 
 |-  ( ( n = N /\ g = G ) -> ( ClWWalks ` g ) = ( ClWWalks ` G ) )
3 eqeq2 
 |-  ( n = N -> ( ( # ` w ) = n <-> ( # ` w ) = N ) )
4 3 adantr 
 |-  ( ( n = N /\ g = G ) -> ( ( # ` w ) = n <-> ( # ` w ) = N ) )
5 2 4 rabeqbidv 
 |-  ( ( n = N /\ g = G ) -> { w e. ( ClWWalks ` g ) | ( # ` w ) = n } = { w e. ( ClWWalks ` G ) | ( # ` w ) = N } )
6 df-clwwlkn 
 |-  ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. ( ClWWalks ` g ) | ( # ` w ) = n } )
7 fvex 
 |-  ( ClWWalks ` G ) e. _V
8 7 rabex 
 |-  { w e. ( ClWWalks ` G ) | ( # ` w ) = N } e. _V
9 5 6 8 ovmpoa 
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N } )
10 6 mpondm0 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N ClWWalksN G ) = (/) )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 11 clwwlkbp 
 |-  ( w e. ( ClWWalks ` G ) -> ( G e. _V /\ w e. Word ( Vtx ` G ) /\ w =/= (/) ) )
13 12 simp2d 
 |-  ( w e. ( ClWWalks ` G ) -> w e. Word ( Vtx ` G ) )
14 lencl 
 |-  ( w e. Word ( Vtx ` G ) -> ( # ` w ) e. NN0 )
15 13 14 syl 
 |-  ( w e. ( ClWWalks ` G ) -> ( # ` w ) e. NN0 )
16 eleq1 
 |-  ( ( # ` w ) = N -> ( ( # ` w ) e. NN0 <-> N e. NN0 ) )
17 15 16 syl5ibcom 
 |-  ( w e. ( ClWWalks ` G ) -> ( ( # ` w ) = N -> N e. NN0 ) )
18 17 con3rr3 
 |-  ( -. N e. NN0 -> ( w e. ( ClWWalks ` G ) -> -. ( # ` w ) = N ) )
19 18 ralrimiv 
 |-  ( -. N e. NN0 -> A. w e. ( ClWWalks ` G ) -. ( # ` w ) = N )
20 ral0 
 |-  A. w e. (/) -. ( # ` w ) = N
21 fvprc 
 |-  ( -. G e. _V -> ( ClWWalks ` G ) = (/) )
22 21 raleqdv 
 |-  ( -. G e. _V -> ( A. w e. ( ClWWalks ` G ) -. ( # ` w ) = N <-> A. w e. (/) -. ( # ` w ) = N ) )
23 20 22 mpbiri 
 |-  ( -. G e. _V -> A. w e. ( ClWWalks ` G ) -. ( # ` w ) = N )
24 19 23 jaoi 
 |-  ( ( -. N e. NN0 \/ -. G e. _V ) -> A. w e. ( ClWWalks ` G ) -. ( # ` w ) = N )
25 ianor 
 |-  ( -. ( N e. NN0 /\ G e. _V ) <-> ( -. N e. NN0 \/ -. G e. _V ) )
26 rabeq0 
 |-  ( { w e. ( ClWWalks ` G ) | ( # ` w ) = N } = (/) <-> A. w e. ( ClWWalks ` G ) -. ( # ` w ) = N )
27 24 25 26 3imtr4i 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( ClWWalks ` G ) | ( # ` w ) = N } = (/) )
28 10 27 eqtr4d 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N } )
29 9 28 pm2.61i 
 |-  ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) | ( # ` w ) = N }