Theorem upgrwlkupwlkb

Description: In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020)

	Ref	Expression
Assertion	upgrwlkupwlkb	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		upgrwlkupwlk	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 )
2	1	ex	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )
3		upwlkwlk	⊢ ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4	2 3	impbid1	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )