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	$$⊢G\in \mathrm{UPGraph}\to \left(F\mathrm{Walks}\left(G\right)P\leftrightarrow F\mathrm{UPWalks}\left(G\right)P\right)$$

Proof

Step	Hyp	Ref	Expression
1		upgrwlkupwlk	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\mathrm{Walks}\left(G\right)P\right)\to F\mathrm{UPWalks}\left(G\right)P$$
2	1	ex	$$⊢G\in \mathrm{UPGraph}\to \left(F\mathrm{Walks}\left(G\right)P\to F\mathrm{UPWalks}\left(G\right)P\right)$$
3		upwlkwlk	$$⊢F\mathrm{UPWalks}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
4	2 3	impbid1	$$⊢G\in \mathrm{UPGraph}\to \left(F\mathrm{Walks}\left(G\right)P\leftrightarrow F\mathrm{UPWalks}\left(G\right)P\right)$$