Metamath Proof Explorer


Theorem wlkcomp

Description: A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-Jan-2021)

Ref Expression
Hypotheses wlkcomp.v
|- V = ( Vtx ` G )
wlkcomp.i
|- I = ( iEdg ` G )
wlkcomp.1
|- F = ( 1st ` W )
wlkcomp.2
|- P = ( 2nd ` W )
Assertion wlkcomp
|- ( ( G e. U /\ W e. ( S X. T ) ) -> ( W e. ( Walks ` G ) <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkcomp.v
 |-  V = ( Vtx ` G )
2 wlkcomp.i
 |-  I = ( iEdg ` G )
3 wlkcomp.1
 |-  F = ( 1st ` W )
4 wlkcomp.2
 |-  P = ( 2nd ` W )
5 3 eqcomi
 |-  ( 1st ` W ) = F
6 4 eqcomi
 |-  ( 2nd ` W ) = P
7 5 6 pm3.2i
 |-  ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P )
8 eqop
 |-  ( W e. ( S X. T ) -> ( W = <. F , P >. <-> ( ( 1st ` W ) = F /\ ( 2nd ` W ) = P ) ) )
9 7 8 mpbiri
 |-  ( W e. ( S X. T ) -> W = <. F , P >. )
10 9 eleq1d
 |-  ( W e. ( S X. T ) -> ( W e. ( Walks ` G ) <-> <. F , P >. e. ( Walks ` G ) ) )
11 df-br
 |-  ( F ( Walks ` G ) P <-> <. F , P >. e. ( Walks ` G ) )
12 10 11 bitr4di
 |-  ( W e. ( S X. T ) -> ( W e. ( Walks ` G ) <-> F ( Walks ` G ) P ) )
13 1 2 iswlkg
 |-  ( G e. U -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
14 12 13 sylan9bbr
 |-  ( ( G e. U /\ W e. ( S X. T ) ) -> ( W e. ( Walks ` G ) <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )