Theorem upgrisupwlkALT

Description: Alternate proof of upgriswlk using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	upgrisupwlkALT.v	|- V = ( Vtx ` G )
	upgrisupwlkALT.i	|- I = ( iEdg ` G )
Assertion	upgrisupwlkALT	|- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		upgrisupwlkALT.v	|- V = ( Vtx ` G )
2		upgrisupwlkALT.i	|- I = ( iEdg ` G )
3		upgrwlkupwlkb	|- ( G e. UPGraph -> ( F ( Walks ` G ) P <-> F ( UPWalks ` G ) P ) )
4	3	3ad2ant1	|- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> F ( UPWalks ` G ) P ) )
5	1 2	isupwlk	|- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
6	4 5	bitrd	|- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )