Metamath Proof Explorer

Theorem clwlknon2num

Description: There are k walks of length 2 on each vertex X in a k-regular simple graph. Variant of clwwlknon2num , using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypothesis clwlknon2num.v 
|- V = ( Vtx ` G )
Assertion clwlknon2num 
|- ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = K )

Proof

Step Hyp Ref Expression
1 clwlknon2num.v 
 |-  V = ( Vtx ` G )
2 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
3 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
4 2 3 syl 
 |-  ( G RegUSGraph K -> G e. USPGraph )
5 4 3ad2ant2 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> G e. USPGraph )
6 1 eleq2i 
 |-  ( X e. V <-> X e. ( Vtx ` G ) )
7 6 biimpi 
 |-  ( X e. V -> X e. ( Vtx ` G ) )
8 7 3ad2ant3 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> X e. ( Vtx ` G ) )
9 2nn 
 |-  2 e. NN
10 9 a1i 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> 2 e. NN )
11 clwwlknonclwlknonen 
 |-  ( ( G e. USPGraph /\ X e. ( Vtx ` G ) /\ 2 e. NN ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) 2 ) )
12 5 8 10 11 syl3anc 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) 2 ) )
13 2 anim2i 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( V e. Fin /\ G e. USGraph ) )
14 13 ancomd 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( G e. USGraph /\ V e. Fin ) )
15 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
16 14 15 sylibr 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> G e. FinUSGraph )
17 16 3adant3 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> G e. FinUSGraph )
18 2nn0 
 |-  2 e. NN0
19 18 a1i 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> 2 e. NN0 )
20 wlksnfi 
 |-  ( ( G e. FinUSGraph /\ 2 e. NN0 ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = 2 } e. Fin )
21 17 19 20 syl2anc 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = 2 } e. Fin )
22 clwlkswks 
 |-  ( ClWalks ` G ) C_ ( Walks ` G )
23 22 a1i 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( ClWalks ` G ) C_ ( Walks ` G ) )
24 simp2l 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) /\ ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) /\ w e. ( ClWalks ` G ) ) -> ( # ` ( 1st ` w ) ) = 2 )
25 23 24 rabssrabd 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } C_ { w e. ( Walks ` G ) | ( # ` ( 1st ` w ) ) = 2 } )
26 21 25 ssfid 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } e. Fin )
27 1 clwwlknonfin 
 |-  ( V e. Fin -> ( X ( ClWWalksNOn ` G ) 2 ) e. Fin )
28 27 3ad2ant1 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( X ( ClWWalksNOn ` G ) 2 ) e. Fin )
29 hashen 
 |-  ( ( { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } e. Fin /\ ( X ( ClWWalksNOn ` G ) 2 ) e. Fin ) -> ( ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) <-> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) 2 ) ) )
30 26 28 29 syl2anc 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) <-> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) 2 ) ) )
31 12 30 mpbird 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) )
32 7 anim2i 
 |-  ( ( G RegUSGraph K /\ X e. V ) -> ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) )
33 32 3adant1 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) )
34 clwwlknon2num 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )
35 33 34 syl 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )
36 31 35 eqtrd 
 |-  ( ( V e. Fin /\ G RegUSGraph K /\ X e. V ) -> ( # ` { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 2 /\ ( ( 2nd ` w ) ` 0 ) = X ) } ) = K )