This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) \to W \in (V \times V)$

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