# Metamath Proof Explorer

## Theorem wlk2v2elem2

Description: Lemma 2 for wlk2v2e : The values of I after F are edges between two vertices enumerated by P . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

Ref Expression
Hypotheses wlk2v2e.i ${⊢}{I}=⟨“\left\{{X},{Y}\right\}”⟩$
wlk2v2e.f ${⊢}{F}=⟨“00”⟩$
wlk2v2e.x ${⊢}{X}\in \mathrm{V}$
wlk2v2e.y ${⊢}{Y}\in \mathrm{V}$
wlk2v2e.p ${⊢}{P}=⟨“{X}{Y}{X}”⟩$
Assertion wlk2v2elem2 ${⊢}\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\}$

### Proof

Step Hyp Ref Expression
1 wlk2v2e.i ${⊢}{I}=⟨“\left\{{X},{Y}\right\}”⟩$
2 wlk2v2e.f ${⊢}{F}=⟨“00”⟩$
3 wlk2v2e.x ${⊢}{X}\in \mathrm{V}$
4 wlk2v2e.y ${⊢}{Y}\in \mathrm{V}$
5 wlk2v2e.p ${⊢}{P}=⟨“{X}{Y}{X}”⟩$
6 2 fveq1i ${⊢}{F}\left(0\right)=⟨“00”⟩\left(0\right)$
7 0z ${⊢}0\in ℤ$
8 s2fv0 ${⊢}0\in ℤ\to ⟨“00”⟩\left(0\right)=0$
9 7 8 ax-mp ${⊢}⟨“00”⟩\left(0\right)=0$
10 6 9 eqtri ${⊢}{F}\left(0\right)=0$
11 10 fveq2i ${⊢}{I}\left({F}\left(0\right)\right)={I}\left(0\right)$
12 1 fveq1i ${⊢}{I}\left(0\right)=⟨“\left\{{X},{Y}\right\}”⟩\left(0\right)$
13 prex ${⊢}\left\{{X},{Y}\right\}\in \mathrm{V}$
14 s1fv ${⊢}\left\{{X},{Y}\right\}\in \mathrm{V}\to ⟨“\left\{{X},{Y}\right\}”⟩\left(0\right)=\left\{{X},{Y}\right\}$
15 13 14 ax-mp ${⊢}⟨“\left\{{X},{Y}\right\}”⟩\left(0\right)=\left\{{X},{Y}\right\}$
16 12 15 eqtri ${⊢}{I}\left(0\right)=\left\{{X},{Y}\right\}$
17 5 fveq1i ${⊢}{P}\left(0\right)=⟨“{X}{Y}{X}”⟩\left(0\right)$
18 s3fv0 ${⊢}{X}\in \mathrm{V}\to ⟨“{X}{Y}{X}”⟩\left(0\right)={X}$
19 3 18 ax-mp ${⊢}⟨“{X}{Y}{X}”⟩\left(0\right)={X}$
20 17 19 eqtri ${⊢}{P}\left(0\right)={X}$
21 5 fveq1i ${⊢}{P}\left(1\right)=⟨“{X}{Y}{X}”⟩\left(1\right)$
22 s3fv1 ${⊢}{Y}\in \mathrm{V}\to ⟨“{X}{Y}{X}”⟩\left(1\right)={Y}$
23 4 22 ax-mp ${⊢}⟨“{X}{Y}{X}”⟩\left(1\right)={Y}$
24 21 23 eqtri ${⊢}{P}\left(1\right)={Y}$
25 20 24 preq12i ${⊢}\left\{{P}\left(0\right),{P}\left(1\right)\right\}=\left\{{X},{Y}\right\}$
26 25 eqcomi ${⊢}\left\{{X},{Y}\right\}=\left\{{P}\left(0\right),{P}\left(1\right)\right\}$
27 11 16 26 3eqtri ${⊢}{I}\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}$
28 2 fveq1i ${⊢}{F}\left(1\right)=⟨“00”⟩\left(1\right)$
29 s2fv1 ${⊢}0\in ℤ\to ⟨“00”⟩\left(1\right)=0$
30 7 29 ax-mp ${⊢}⟨“00”⟩\left(1\right)=0$
31 28 30 eqtri ${⊢}{F}\left(1\right)=0$
32 31 fveq2i ${⊢}{I}\left({F}\left(1\right)\right)={I}\left(0\right)$
33 prcom ${⊢}\left\{{X},{Y}\right\}=\left\{{Y},{X}\right\}$
34 5 fveq1i ${⊢}{P}\left(2\right)=⟨“{X}{Y}{X}”⟩\left(2\right)$
35 s3fv2 ${⊢}{X}\in \mathrm{V}\to ⟨“{X}{Y}{X}”⟩\left(2\right)={X}$
36 3 35 ax-mp ${⊢}⟨“{X}{Y}{X}”⟩\left(2\right)={X}$
37 34 36 eqtri ${⊢}{P}\left(2\right)={X}$
38 24 37 preq12i ${⊢}\left\{{P}\left(1\right),{P}\left(2\right)\right\}=\left\{{Y},{X}\right\}$
39 38 eqcomi ${⊢}\left\{{Y},{X}\right\}=\left\{{P}\left(1\right),{P}\left(2\right)\right\}$
40 33 39 eqtri ${⊢}\left\{{X},{Y}\right\}=\left\{{P}\left(1\right),{P}\left(2\right)\right\}$
41 32 16 40 3eqtri ${⊢}{I}\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}$
42 2wlklem ${⊢}\forall {k}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}↔\left({I}\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge {I}\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)$
43 27 41 42 mpbir2an ${⊢}\forall {k}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}$
44 5 2 2wlkdlem2 ${⊢}\left(0..^\left|{F}\right|\right)=\left\{0,1\right\}$
45 44 raleqi ${⊢}\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\}↔\forall {k}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{I}\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}$
46 43 45 mpbir ${⊢}\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\}$