# Metamath Proof Explorer

## Theorem ewlkprop

Description: Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion ewlkprop ${⊢}{F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)$

### Proof

Step Hyp Ref Expression
1 ewlksfval.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
2 df-ewlks
3 2 elmpocl ${⊢}{F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)$
4 simpr ${⊢}\left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)\wedge \left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\right)\to \left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)$
5 1 isewlk ${⊢}\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\wedge {F}\in \left({G}\mathrm{EdgWalks}{S}\right)\right)\to \left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)↔\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)$
6 5 3expa ${⊢}\left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \left({G}\mathrm{EdgWalks}{S}\right)\right)\to \left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)↔\left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)$
7 6 biimpd ${⊢}\left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \left({G}\mathrm{EdgWalks}{S}\right)\right)\to \left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)$
8 7 expcom ${⊢}{F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\to \left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)\right)$
9 8 pm2.43a ${⊢}{F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)$
10 9 imp ${⊢}\left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)\wedge \left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)$
11 3anass ${⊢}\left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)↔\left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge \left({F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)\right)$
12 4 10 11 sylanbrc ${⊢}\left({F}\in \left({G}\mathrm{EdgWalks}{S}\right)\wedge \left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\right)\to \left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)$
13 3 12 mpdan ${⊢}{F}\in \left({G}\mathrm{EdgWalks}{S}\right)\to \left(\left({G}\in \mathrm{V}\wedge {S}\in {ℕ}_{0}^{*}\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}{I}\wedge \forall {k}\in \left(1..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{S}\le \left|{I}\left({F}\left({k}-1\right)\right)\cap {I}\left({F}\left({k}\right)\right)\right|\right)$