Metamath Proof Explorer

Theorem upgrwlkupwlkb

Description: In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020)

Ref Expression
Assertion upgrwlkupwlkb 
|- ( G e. UPGraph -> ( F ( Walks ` G ) P <-> F ( UPWalks ` G ) P ) )

Proof

Step Hyp Ref Expression
1 upgrwlkupwlk 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> F ( UPWalks ` G ) P )
2 1 ex 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P -> F ( UPWalks ` G ) P ) )
3 upwlkwlk 
 |-  ( F ( UPWalks ` G ) P -> F ( Walks ` G ) P )
4 2 3 impbid1 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> F ( UPWalks ` G ) P ) )