Metamath Proof Explorer


Theorem upwlkbprop

Description: Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 29-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v
|- V = ( Vtx ` G )
upwlksfval.i
|- I = ( iEdg ` G )
Assertion upwlkbprop
|- ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )

Proof

Step Hyp Ref Expression
1 upwlksfval.v
 |-  V = ( Vtx ` G )
2 upwlksfval.i
 |-  I = ( iEdg ` G )
3 1 2 upwlksfval
 |-  ( G e. _V -> ( UPWalks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } )
4 3 breqd
 |-  ( G e. _V -> ( F ( UPWalks ` G ) P <-> F { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } P ) )
5 brabv
 |-  ( F { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } P -> ( F e. _V /\ P e. _V ) )
6 4 5 syl6bi
 |-  ( G e. _V -> ( F ( UPWalks ` G ) P -> ( F e. _V /\ P e. _V ) ) )
7 6 imdistani
 |-  ( ( G e. _V /\ F ( UPWalks ` G ) P ) -> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) )
8 3anass
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) <-> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) )
9 7 8 sylibr
 |-  ( ( G e. _V /\ F ( UPWalks ` G ) P ) -> ( G e. _V /\ F e. _V /\ P e. _V ) )
10 9 ex
 |-  ( G e. _V -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) )
11 fvprc
 |-  ( -. G e. _V -> ( UPWalks ` G ) = (/) )
12 breq
 |-  ( ( UPWalks ` G ) = (/) -> ( F ( UPWalks ` G ) P <-> F (/) P ) )
13 br0
 |-  -. F (/) P
14 13 pm2.21i
 |-  ( F (/) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
15 12 14 syl6bi
 |-  ( ( UPWalks ` G ) = (/) -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) )
16 11 15 syl
 |-  ( -. G e. _V -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) )
17 10 16 pm2.61i
 |-  ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )