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 ) )

Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem3

Proof