# Metamath Proof Explorer

## Theorem upwlkbprop

Description: Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 29-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upwlksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion upwlkbprop ${⊢}{F}\mathrm{UPWalks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 upwlksfval.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upwlksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 1 2 upwlksfval ${⊢}{G}\in \mathrm{V}\to \mathrm{UPWalks}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\in \mathrm{Word}\mathrm{dom}{I}\wedge {p}:\left(0\dots \left|{f}\right|\right)⟶{V}\wedge \forall {k}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}{I}\left({f}\left({k}\right)\right)=\left\{{p}\left({k}\right),{p}\left({k}+1\right)\right\}\right)\right\}$
4 3 breqd ${⊢}{G}\in \mathrm{V}\to \left({F}\mathrm{UPWalks}\left({G}\right){P}↔{F}\left\{⟨{f},{p}⟩|\left({f}\in \mathrm{Word}\mathrm{dom}{I}\wedge {p}:\left(0\dots \left|{f}\right|\right)⟶{V}\wedge \forall {k}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}{I}\left({f}\left({k}\right)\right)=\left\{{p}\left({k}\right),{p}\left({k}+1\right)\right\}\right)\right\}{P}\right)$
5 brabv ${⊢}{F}\left\{⟨{f},{p}⟩|\left({f}\in \mathrm{Word}\mathrm{dom}{I}\wedge {p}:\left(0\dots \left|{f}\right|\right)⟶{V}\wedge \forall {k}\in \left(0..^\left|{f}\right|\right)\phantom{\rule{.4em}{0ex}}{I}\left({f}\left({k}\right)\right)=\left\{{p}\left({k}\right),{p}\left({k}+1\right)\right\}\right)\right\}{P}\to \left({F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
6 4 5 syl6bi ${⊢}{G}\in \mathrm{V}\to \left({F}\mathrm{UPWalks}\left({G}\right){P}\to \left({F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
7 6 imdistani ${⊢}\left({G}\in \mathrm{V}\wedge {F}\mathrm{UPWalks}\left({G}\right){P}\right)\to \left({G}\in \mathrm{V}\wedge \left({F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
8 3anass ${⊢}\left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)↔\left({G}\in \mathrm{V}\wedge \left({F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
9 7 8 sylibr ${⊢}\left({G}\in \mathrm{V}\wedge {F}\mathrm{UPWalks}\left({G}\right){P}\right)\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
10 9 ex ${⊢}{G}\in \mathrm{V}\to \left({F}\mathrm{UPWalks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
11 fvprc ${⊢}¬{G}\in \mathrm{V}\to \mathrm{UPWalks}\left({G}\right)=\varnothing$
12 breq ${⊢}\mathrm{UPWalks}\left({G}\right)=\varnothing \to \left({F}\mathrm{UPWalks}\left({G}\right){P}↔{F}\varnothing {P}\right)$
13 br0 ${⊢}¬{F}\varnothing {P}$
14 13 pm2.21i ${⊢}{F}\varnothing {P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
15 12 14 syl6bi ${⊢}\mathrm{UPWalks}\left({G}\right)=\varnothing \to \left({F}\mathrm{UPWalks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
16 11 15 syl ${⊢}¬{G}\in \mathrm{V}\to \left({F}\mathrm{UPWalks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\right)$
17 10 16 pm2.61i ${⊢}{F}\mathrm{UPWalks}\left({G}\right){P}\to \left({G}\in \mathrm{V}\wedge {F}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$