This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwlkclwwlken

Description: The set of the nonempty closed walks and the set of closed walks as word are equinumerous in a simple pseudograph. (Contributed by AV, 25-May-2022) (Proof shortened by AV, 4-Nov-2022)

Ref Expression
Assertion clwlkclwwlken 
|- ( G e. USPGraph -> { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ~~ ( ClWWalks ` G ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( ClWalks ` G ) e. _V
2 1 rabex 
 |-  { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } e. _V
3 fvex 
 |-  ( ClWWalks ` G ) e. _V
4 2fveq3 
 |-  ( w = u -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` u ) ) )
5 4 breq2d 
 |-  ( w = u -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ ( # ` ( 1st ` u ) ) ) )
6 5 cbvrabv 
 |-  { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } = { u e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` u ) ) }
7 fveq2 
 |-  ( d = c -> ( 2nd ` d ) = ( 2nd ` c ) )
8 2fveq3 
 |-  ( d = c -> ( # ` ( 2nd ` d ) ) = ( # ` ( 2nd ` c ) ) )
9 8 oveq1d 
 |-  ( d = c -> ( ( # ` ( 2nd ` d ) ) - 1 ) = ( ( # ` ( 2nd ` c ) ) - 1 ) )
10 7 9 oveq12d 
 |-  ( d = c -> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) = ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
11 10 cbvmptv 
 |-  ( d e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) = ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
12 6 11 clwlkclwwlkf1o 
 |-  ( G e. USPGraph -> ( d e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) : { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -1-1-onto-> ( ClWWalks ` G ) )
13 f1oen2g 
 |-  ( ( { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } e. _V /\ ( ClWWalks ` G ) e. _V /\ ( d e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( ( 2nd ` d ) prefix ( ( # ` ( 2nd ` d ) ) - 1 ) ) ) : { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } -1-1-onto-> ( ClWWalks ` G ) ) -> { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ~~ ( ClWWalks ` G ) )
14 2 3 12 13 mp3an12i 
 |-  ( G e. USPGraph -> { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } ~~ ( ClWWalks ` G ) )