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	biimtrdi	|- ( 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	biimtrdi	|- ( ( 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 ) )