Metamath Proof Explorer

Theorem clwwlknonclwlknonen

Description: The sets of the two representations of closed walks of a fixed positive length on a fixed vertex are equinumerous. (Contributed by AV, 27-May-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Assertion clwwlknonclwlknonen 
|- ( ( G e. USPGraph /\ X e. ( Vtx ` G ) /\ N e. NN ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) N ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( ClWalks ` G ) e. _V
2 1 rabex 
 |-  { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } e. _V
3 ovex 
 |-  ( X ( ClWWalksNOn ` G ) N ) e. _V
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) }
6 eqid 
 |-  ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) = ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) )
7 4 5 6 clwwlknonclwlknonf1o 
 |-  ( ( G e. USPGraph /\ X e. ( Vtx ` G ) /\ N e. NN ) -> ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) )
8 f1oen2g 
 |-  ( ( { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } e. _V /\ ( X ( ClWWalksNOn ` G ) N ) e. _V /\ ( c e. { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } |-> ( ( 2nd ` c ) prefix ( # ` ( 1st ` c ) ) ) ) : { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } -1-1-onto-> ( X ( ClWWalksNOn ` G ) N ) ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) N ) )
9 2 3 7 8 mp3an12i 
 |-  ( ( G e. USPGraph /\ X e. ( Vtx ` G ) /\ N e. NN ) -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X ) } ~~ ( X ( ClWWalksNOn ` G ) N ) )