Metamath Proof Explorer

Theorem wlkcpr

Description: A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlkcpr 
|- ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )

Proof

Step Hyp Ref Expression
1 wlkop 
 |-  ( W e. ( Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
2 wlkvv 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> W e. ( _V X. _V ) )
3 1st2ndb 
 |-  ( W e. ( _V X. _V ) <-> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
4 2 3 sylib 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
5 eleq1 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. ( Walks ` G ) <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. ( Walks ` G ) ) )
6 df-br 
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) <-> <. ( 1st ` W ) , ( 2nd ` W ) >. e. ( Walks ` G ) )
7 5 6 bitr4di 
 |-  ( W = <. ( 1st ` W ) , ( 2nd ` W ) >. -> ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) )
8 1 4 7 pm5.21nii 
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )