Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem3

Description: Lemma 3 for clwlknf1oclwwlkn : The bijective function of clwlknf1oclwwlkn is the bijective function of clwlkclwwlkf1o restricted to the closed walks with a fixed positive length. (Contributed by AV, 26-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwlknf1oclwwlkn.a 
|- A = ( 1st ` c )
clwlknf1oclwwlkn.b 
|- B = ( 2nd ` c )
clwlknf1oclwwlkn.c 
|- C = { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N }
clwlknf1oclwwlkn.f 
|- F = ( c e. C |-> ( B prefix ( # ` A ) ) )
Assertion clwlknf1oclwwlknlem3 
|- ( ( G e. USPGraph /\ N e. NN ) -> F = ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) |` C ) )

Proof

Step Hyp Ref Expression
1 clwlknf1oclwwlkn.a 
 |-  A = ( 1st ` c )
2 clwlknf1oclwwlkn.b 
 |-  B = ( 2nd ` c )
3 clwlknf1oclwwlkn.c 
 |-  C = { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N }
4 clwlknf1oclwwlkn.f 
 |-  F = ( c e. C |-> ( B prefix ( # ` A ) ) )
5 nnge1 
 |-  ( N e. NN -> 1 <_ N )
6 breq2 
 |-  ( ( # ` ( 1st ` w ) ) = N -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ N ) )
7 5 6 syl5ibrcom 
 |-  ( N e. NN -> ( ( # ` ( 1st ` w ) ) = N -> 1 <_ ( # ` ( 1st ` w ) ) ) )
8 7 ad2antlr 
 |-  ( ( ( G e. USPGraph /\ N e. NN ) /\ w e. ( ClWalks ` G ) ) -> ( ( # ` ( 1st ` w ) ) = N -> 1 <_ ( # ` ( 1st ` w ) ) ) )
9 8 ss2rabdv 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } C_ { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } )
10 3 9 eqsstrid 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> C C_ { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } )
11 10 resmptd 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) |` C ) = ( c e. C |-> ( B prefix ( # ` A ) ) ) )
12 4 11 eqtr4id 
 |-  ( ( G e. USPGraph /\ N e. NN ) -> F = ( ( c e. { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } |-> ( B prefix ( # ` A ) ) ) |` C ) )