This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → if- P ⁡ A = P ⁡ A + 1 I ⁡ F ⁡ A = P ⁡ A P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ if- P ⁡ B = P ⁡ B + 1 I ⁡ F ⁡ B = P ⁡ B P ⁡ B P ⁡ B + 1 ⊆ I ⁡ F ⁡ B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = B → P ⁡ A = P ⁡ B
2 fvoveq1 ⊢ A = B → P ⁡ A + 1 = P ⁡ B + 1
3 1 2 eqeq12d ⊢ A = B → P ⁡ A = P ⁡ A + 1 ↔ P ⁡ B = P ⁡ B + 1
4 2fveq3 ⊢ A = B → I ⁡ F ⁡ A = I ⁡ F ⁡ B
5 1 sneqd ⊢ A = B → P ⁡ A = P ⁡ B
6 4 5 eqeq12d ⊢ A = B → I ⁡ F ⁡ A = P ⁡ A ↔ I ⁡ F ⁡ B = P ⁡ B
7 1 2 preq12d ⊢ A = B → P ⁡ A P ⁡ A + 1 = P ⁡ B P ⁡ B + 1
8 7 4 sseq12d ⊢ A = B → P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ P ⁡ B P ⁡ B + 1 ⊆ I ⁡ F ⁡ B
9 3 6 8 ifpbi123d ⊢ A = B → if- P ⁡ A = P ⁡ A + 1 I ⁡ F ⁡ A = P ⁡ A P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ if- P ⁡ B = P ⁡ B + 1 I ⁡ F ⁡ B = P ⁡ B P ⁡ B P ⁡ B + 1 ⊆ I ⁡ F ⁡ B