Step |
Hyp |
Ref |
Expression |
1 |
|
uspgrupgr |
|- ( G e. USPGraph -> G e. UPGraph ) |
2 |
|
wlklnwwlkln1 |
|- ( G e. UPGraph -> ( ( f ( Walks ` G ) P /\ ( # ` f ) = N ) -> P e. ( N WWalksN G ) ) ) |
3 |
1 2
|
syl |
|- ( G e. USPGraph -> ( ( f ( Walks ` G ) P /\ ( # ` f ) = N ) -> P e. ( N WWalksN G ) ) ) |
4 |
3
|
exlimdv |
|- ( G e. USPGraph -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) -> P e. ( N WWalksN G ) ) ) |
5 |
|
wlklnwwlkln2 |
|- ( G e. USPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) |
6 |
4 5
|
impbid |
|- ( G e. USPGraph -> ( E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) <-> P e. ( N WWalksN G ) ) ) |