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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgrisupwlkALT.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	upgrisupwlkALT	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		upgrisupwlkALT.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgrisupwlkALT.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		upgrwlkupwlkb	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )
4	3	3ad2ant1	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )
5	1 2	isupwlk	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
6	4 5	bitrd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )