Metamath Proof Explorer


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 W Walks G 2 nd W W V × V

Proof

Step Hyp Ref Expression
1 wlkn0 1 st W Walks G 2 nd W 2 nd W
2 2ndnpr ¬ W V × V 2 nd W =
3 2 necon1ai 2 nd W W V × V
4 1 3 syl 1 st W Walks G 2 nd W W V × V