# Metamath Proof Explorer

## Theorem wlkiswwlks2lem1

Description: Lemma 1 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f ${⊢}{F}=\left({x}\in \left(0..^\left|{P}\right|-1\right)⟼{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left({x}+1\right)\right\}\right)\right)$
Assertion wlkiswwlks2lem1 ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 1\le \left|{P}\right|\right)\to \left|{F}\right|=\left|{P}\right|-1$

### Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ${⊢}{F}=\left({x}\in \left(0..^\left|{P}\right|-1\right)⟼{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left({x}+1\right)\right\}\right)\right)$
2 lencl ${⊢}{P}\in \mathrm{Word}{V}\to \left|{P}\right|\in {ℕ}_{0}$
3 elnnnn0c ${⊢}\left|{P}\right|\in ℕ↔\left(\left|{P}\right|\in {ℕ}_{0}\wedge 1\le \left|{P}\right|\right)$
4 3 biimpri ${⊢}\left(\left|{P}\right|\in {ℕ}_{0}\wedge 1\le \left|{P}\right|\right)\to \left|{P}\right|\in ℕ$
5 2 4 sylan ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 1\le \left|{P}\right|\right)\to \left|{P}\right|\in ℕ$
6 nnm1nn0 ${⊢}\left|{P}\right|\in ℕ\to \left|{P}\right|-1\in {ℕ}_{0}$
7 5 6 syl ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 1\le \left|{P}\right|\right)\to \left|{P}\right|-1\in {ℕ}_{0}$
8 fvex ${⊢}{{E}}^{-1}\left(\left\{{P}\left({x}\right),{P}\left({x}+1\right)\right\}\right)\in \mathrm{V}$
9 8 1 fnmpti ${⊢}{F}Fn\left(0..^\left|{P}\right|-1\right)$
10 ffzo0hash ${⊢}\left(\left|{P}\right|-1\in {ℕ}_{0}\wedge {F}Fn\left(0..^\left|{P}\right|-1\right)\right)\to \left|{F}\right|=\left|{P}\right|-1$
11 7 9 10 sylancl ${⊢}\left({P}\in \mathrm{Word}{V}\wedge 1\le \left|{P}\right|\right)\to \left|{F}\right|=\left|{P}\right|-1$