Metamath Proof Explorer

Theorem wlk2f

Description: If there is a walk W there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018)

Ref Expression
Assertion wlk2f 
|- ( W e. ( Walks ` G ) -> E. f E. p f ( Walks ` G ) p )

Proof

Step Hyp Ref Expression
1 wlkcpr 
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
2 fvex 
 |-  ( 1st ` W ) e. _V
3 fvex 
 |-  ( 2nd ` W ) e. _V
4 breq12 
 |-  ( ( f = ( 1st ` W ) /\ p = ( 2nd ` W ) ) -> ( f ( Walks ` G ) p <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) )
5 2 3 4 spc2ev 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> E. f E. p f ( Walks ` G ) p )
6 1 5 sylbi 
 |-  ( W e. ( Walks ` G ) -> E. f E. p f ( Walks ` G ) p )