Theorem wkslem1

Description: Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021)

	Ref	Expression
Assertion	wkslem1	$$⊢A=B\to \left(if-\left(P\left(A\right)=P\left(A+1\right),I\left(F\left(A\right)\right)=\left\{P\left(A\right)\right\},\left\{P\left(A\right),P\left(A+1\right)\right\}\subseteq I\left(F\left(A\right)\right)\right)\leftrightarrow if-\left(P\left(B\right)=P\left(B+1\right),I\left(F\left(B\right)\right)=\left\{P\left(B\right)\right\},\left\{P\left(B\right),P\left(B+1\right)\right\}\subseteq I\left(F\left(B\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=B\to P\left(A\right)=P\left(B\right)$$
2		fvoveq1	$$⊢A=B\to P\left(A+1\right)=P\left(B+1\right)$$
3	1 2	eqeq12d	$$⊢A=B\to \left(P\left(A\right)=P\left(A+1\right)\leftrightarrow P\left(B\right)=P\left(B+1\right)\right)$$
4		2fveq3	$$⊢A=B\to I\left(F\left(A\right)\right)=I\left(F\left(B\right)\right)$$
5	1	sneqd	$$⊢A=B\to \left\{P\left(A\right)\right\}=\left\{P\left(B\right)\right\}$$
6	4 5	eqeq12d	$$⊢A=B\to \left(I\left(F\left(A\right)\right)=\left\{P\left(A\right)\right\}\leftrightarrow I\left(F\left(B\right)\right)=\left\{P\left(B\right)\right\}\right)$$
7	1 2	preq12d	$$⊢A=B\to \left\{P\left(A\right),P\left(A+1\right)\right\}=\left\{P\left(B\right),P\left(B+1\right)\right\}$$
8	7 4	sseq12d	$$⊢A=B\to \left(\left\{P\left(A\right),P\left(A+1\right)\right\}\subseteq I\left(F\left(A\right)\right)\leftrightarrow \left\{P\left(B\right),P\left(B+1\right)\right\}\subseteq I\left(F\left(B\right)\right)\right)$$
9	3 6 8	ifpbi123d	$$⊢A=B\to \left(if-\left(P\left(A\right)=P\left(A+1\right),I\left(F\left(A\right)\right)=\left\{P\left(A\right)\right\},\left\{P\left(A\right),P\left(A+1\right)\right\}\subseteq I\left(F\left(A\right)\right)\right)\leftrightarrow if-\left(P\left(B\right)=P\left(B+1\right),I\left(F\left(B\right)\right)=\left\{P\left(B\right)\right\},\left\{P\left(B\right),P\left(B+1\right)\right\}\subseteq I\left(F\left(B\right)\right)\right)\right)$$