Theorem wlkvv

Description: If there is at least one walk in the graph, all walks are in the universal class of ordered pairs. (Contributed by AV, 2-Jan-2021)

	Ref	Expression
Assertion	wlkvv	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\to W\in \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		wlkn0	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\to 2^{nd}\left(W\right)\ne \varnothing$$
2		2ndnpr	$$⊢\neg W\in \left(\mathrm{V}\times \mathrm{V}\right)\to 2^{nd}\left(W\right)=\varnothing$$
3	2	necon1ai	$$⊢2^{nd}\left(W\right)\ne \varnothing \to W\in \left(\mathrm{V}\times \mathrm{V}\right)$$
4	1 3	syl	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\to W\in \left(\mathrm{V}\times \mathrm{V}\right)$$