Theorem wwlksnon0

Description: Sufficient conditions for a set of walks of a fixed length between two vertices to be empty. (Contributed by AV, 15-May-2021) (Proof shortened by AV, 21-May-2021)

	Ref	Expression
Hypothesis	wwlksnon0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	wwlksnon0	$$⊢\neg \left(\left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\wedge \left(A\in V\wedge B\in V\right)\right)\to A\left(N\mathrm{WWalksNOn}G\right)B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		wwlksnon0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		df-wwlksnon	$$⊢\mathrm{WWalksNOn}=\left(n\in {\mathbb{N}}_0,g\in \mathrm{V}⟼\left(a\in \mathrm{Vtx}\left(g\right),b\in \mathrm{Vtx}\left(g\right)⟼\left\{w\in \left(n\mathrm{WWalksN}g\right)|\left(w\left(0\right)=a\wedge w\left(n\right)=b\right)\right\}\right)\right)$$
3	1	wwlksnon	$$⊢\left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\to N\mathrm{WWalksNOn}G=\left(a\in V,b\in V⟼\left\{w\in \left(N\mathrm{WWalksN}G\right)|\left(w\left(0\right)=a\wedge w\left(N\right)=b\right)\right\}\right)$$
4	2 3	2mpo0	$$⊢\neg \left(\left(N\in {\mathbb{N}}_0\wedge G\in \mathrm{V}\right)\wedge \left(A\in V\wedge B\in V\right)\right)\to A\left(N\mathrm{WWalksNOn}G\right)B=\varnothing$$