Theorem 2wlklem

Description: Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018)

	Ref	Expression
Assertion	2wlklem	$$⊢\forall k\in \left\{0,1\right\}E\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow \left(E\left(F\left(0\right)\right)=\left\{P\left(0\right),P\left(1\right)\right\}\wedge E\left(F\left(1\right)\right)=\left\{P\left(1\right),P\left(2\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$$⊢0\in \mathrm{V}$$
2		1ex	$$⊢1\in \mathrm{V}$$
3		2fveq3	$$⊢k=0\to E\left(F\left(k\right)\right)=E\left(F\left(0\right)\right)$$
4		fveq2	$$⊢k=0\to P\left(k\right)=P\left(0\right)$$
5		fv0p1e1	$$⊢k=0\to P\left(k+1\right)=P\left(1\right)$$
6	4 5	preq12d	$$⊢k=0\to \left\{P\left(k\right),P\left(k+1\right)\right\}=\left\{P\left(0\right),P\left(1\right)\right\}$$
7	3 6	eqeq12d	$$⊢k=0\to \left(E\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow E\left(F\left(0\right)\right)=\left\{P\left(0\right),P\left(1\right)\right\}\right)$$
8		2fveq3	$$⊢k=1\to E\left(F\left(k\right)\right)=E\left(F\left(1\right)\right)$$
9		fveq2	$$⊢k=1\to P\left(k\right)=P\left(1\right)$$
10		oveq1	$$⊢k=1\to k+1=1+1$$
11		1p1e2	$$⊢1+1=2$$
12	10 11	eqtrdi	$$⊢k=1\to k+1=2$$
13	12	fveq2d	$$⊢k=1\to P\left(k+1\right)=P\left(2\right)$$
14	9 13	preq12d	$$⊢k=1\to \left\{P\left(k\right),P\left(k+1\right)\right\}=\left\{P\left(1\right),P\left(2\right)\right\}$$
15	8 14	eqeq12d	$$⊢k=1\to \left(E\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow E\left(F\left(1\right)\right)=\left\{P\left(1\right),P\left(2\right)\right\}\right)$$
16	1 2 7 15	ralpr	$$⊢\forall k\in \left\{0,1\right\}E\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow \left(E\left(F\left(0\right)\right)=\left\{P\left(0\right),P\left(1\right)\right\}\wedge E\left(F\left(1\right)\right)=\left\{P\left(1\right),P\left(2\right)\right\}\right)$$