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 ` W ) ( Walks ` G ) ( 2nd ` W ) -> W e. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		wlkn0	|- ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 2nd ` W ) =/= (/) )
2		2ndnpr	|- ( -. W e. ( _V X. _V ) -> ( 2nd ` W ) = (/) )
3	2	necon1ai	|- ( ( 2nd ` W ) =/= (/) -> W e. ( _V X. _V ) )
4	1 3	syl	|- ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> W e. ( _V X. _V ) )