# Metamath Proof Explorer

## Theorem iswwlksnon

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis iswwlksnon.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion iswwlksnon ${⊢}{A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 iswwlksnon.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 0ov ${⊢}{A}\varnothing {B}=\varnothing$
3 df-wwlksnon ${⊢}\mathrm{WWalksNOn}=\left({n}\in {ℕ}_{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)$
4 3 mpondm0 ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to {N}\mathrm{WWalksNOn}{G}=\varnothing$
5 4 oveqd ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}={A}\varnothing {B}$
6 df-wwlksn ${⊢}\mathrm{WWalksN}=\left({n}\in {ℕ}_{0},{g}\in \mathrm{V}⟼\left\{{w}\in \mathrm{WWalks}\left({g}\right)|\left|{w}\right|={n}+1\right\}\right)$
7 6 mpondm0 ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to {N}\mathrm{WWalksN}{G}=\varnothing$
8 7 rabeqdv ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}=\left\{{w}\in \varnothing |\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
9 rab0 ${⊢}\left\{{w}\in \varnothing |\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}=\varnothing$
10 8 9 syl6eq ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}=\varnothing$
11 2 5 10 3eqtr4a ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
12 1 wwlksnon ${⊢}\left({N}\in {ℕ}_{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)$
13 12 adantr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge ¬\left({A}\in {V}\wedge {B}\in {V}\right)\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)$
14 13 oveqd ${⊢}\left(\left({N}\in {ℕ}_{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}={A}\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){B}$
15 eqid ${⊢}\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)=\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)$
16 15 mpondm0 ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\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){B}=\varnothing$
17 16 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge ¬\left({A}\in {V}\wedge {B}\in {V}\right)\right)\to {A}\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){B}=\varnothing$
18 14 17 eqtrd ${⊢}\left(\left({N}\in {ℕ}_{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$
19 18 ex ${⊢}\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to \left(¬\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\varnothing \right)$
20 5 2 syl6eq ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\varnothing$
21 20 a1d ${⊢}¬\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\to \left(¬\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\varnothing \right)$
22 19 21 pm2.61i ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\varnothing$
23 1 wwlknllvtx ${⊢}{w}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({w}\left(0\right)\in {V}\wedge {w}\left({N}\right)\in {V}\right)$
24 eleq1 ${⊢}{A}={w}\left(0\right)\to \left({A}\in {V}↔{w}\left(0\right)\in {V}\right)$
25 24 eqcoms ${⊢}{w}\left(0\right)={A}\to \left({A}\in {V}↔{w}\left(0\right)\in {V}\right)$
26 eleq1 ${⊢}{B}={w}\left({N}\right)\to \left({B}\in {V}↔{w}\left({N}\right)\in {V}\right)$
27 26 eqcoms ${⊢}{w}\left({N}\right)={B}\to \left({B}\in {V}↔{w}\left({N}\right)\in {V}\right)$
28 25 27 bi2anan9 ${⊢}\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)↔\left({w}\left(0\right)\in {V}\wedge {w}\left({N}\right)\in {V}\right)\right)$
29 23 28 syl5ibrcom ${⊢}{w}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left(\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\to \left({A}\in {V}\wedge {B}\in {V}\right)\right)$
30 29 con3rr3 ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({w}\in \left({N}\mathrm{WWalksN}{G}\right)\to ¬\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right)$
31 30 ralrimiv ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to \forall {w}\in \left({N}\mathrm{WWalksN}{G}\right)\phantom{\rule{.4em}{0ex}}¬\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)$
32 rabeq0 ${⊢}\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}=\varnothing ↔\forall {w}\in \left({N}\mathrm{WWalksN}{G}\right)\phantom{\rule{.4em}{0ex}}¬\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)$
33 31 32 sylibr ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}=\varnothing$
34 22 33 eqtr4d ${⊢}¬\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
35 12 adantr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\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)$
36 eqeq2 ${⊢}{a}={A}\to \left({w}\left(0\right)={a}↔{w}\left(0\right)={A}\right)$
37 eqeq2 ${⊢}{b}={B}\to \left({w}\left({N}\right)={b}↔{w}\left({N}\right)={B}\right)$
38 36 37 bi2anan9 ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left(\left({w}\left(0\right)={a}\wedge {w}\left({N}\right)={b}\right)↔\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right)$
39 38 rabbidv ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={a}\wedge {w}\left({N}\right)={b}\right)\right\}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
40 39 adantl ${⊢}\left(\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\wedge \left({a}={A}\wedge {b}={B}\right)\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={a}\wedge {w}\left({N}\right)={b}\right)\right\}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
41 simprl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to {A}\in {V}$
42 simprr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to {B}\in {V}$
43 ovex ${⊢}{N}\mathrm{WWalksN}{G}\in \mathrm{V}$
44 43 rabex ${⊢}\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}\in \mathrm{V}$
45 44 a1i ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {G}\in \mathrm{V}\right)\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}\in \mathrm{V}$
46 35 40 41 42 45 ovmpod ${⊢}\left(\left({N}\in {ℕ}_{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}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$
47 11 34 46 ecase ${⊢}{A}\left({N}\mathrm{WWalksNOn}{G}\right){B}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\left({w}\left(0\right)={A}\wedge {w}\left({N}\right)={B}\right)\right\}$