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