Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem2

Description: Lemma 2 for clwlknf1oclwwlkn : The closed walks of a positive length are nonempty closed walks of this length. (Contributed by AV, 26-May-2022)

Ref Expression
Assertion clwlknf1oclwwlknlem2 
|- ( N e. NN -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( w = c -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` c ) ) )
2 1 eqeq1d 
 |-  ( w = c -> ( ( # ` ( 1st ` w ) ) = N <-> ( # ` ( 1st ` c ) ) = N ) )
3 2 cbvrabv 
 |-  { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N }
4 nnge1 
 |-  ( N e. NN -> 1 <_ N )
5 breq2 
 |-  ( ( # ` ( 1st ` c ) ) = N -> ( 1 <_ ( # ` ( 1st ` c ) ) <-> 1 <_ N ) )
6 4 5 syl5ibrcom 
 |-  ( N e. NN -> ( ( # ` ( 1st ` c ) ) = N -> 1 <_ ( # ` ( 1st ` c ) ) ) )
7 6 pm4.71rd 
 |-  ( N e. NN -> ( ( # ` ( 1st ` c ) ) = N <-> ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) ) )
8 7 rabbidv 
 |-  ( N e. NN -> { c e. ( ClWalks ` G ) | ( # ` ( 1st ` c ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )
9 3 8 syl5eq 
 |-  ( N e. NN -> { w e. ( ClWalks ` G ) | ( # ` ( 1st ` w ) ) = N } = { c e. ( ClWalks ` G ) | ( 1 <_ ( # ` ( 1st ` c ) ) /\ ( # ` ( 1st ` c ) ) = N ) } )