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	⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → 𝑊 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		wlkn0	⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → ( 2nd ‘ 𝑊 ) ≠ ∅ )
2		2ndnpr	⊢ ( ¬ 𝑊 ∈ ( V × V ) → ( 2nd ‘ 𝑊 ) = ∅ )
3	2	necon1ai	⊢ ( ( 2nd ‘ 𝑊 ) ≠ ∅ → 𝑊 ∈ ( V × V ) )
4	1 3	syl	⊢ ( ( 1st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑊 ) → 𝑊 ∈ ( V × V ) )