Metamath Proof Explorer

Theorem wkslem2

Description: Lemma 2 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 wkslem2 ⊢ A = B ∧ A + 1 = C → if- P ⁡ A = P ⁡ A + 1 I ⁡ F ⁡ A = P ⁡ A P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ if- P ⁡ B = P ⁡ C I ⁡ F ⁡ B = P ⁡ B P ⁡ B P ⁡ C ⊆ I ⁡ F ⁡ B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = B → P ⁡ A = P ⁡ B
2 1 adantr ⊢ A = B ∧ A + 1 = C → P ⁡ A = P ⁡ B
3 fveq2 ⊢ A + 1 = C → P ⁡ A + 1 = P ⁡ C
4 3 adantl ⊢ A = B ∧ A + 1 = C → P ⁡ A + 1 = P ⁡ C
5 2 4 eqeq12d ⊢ A = B ∧ A + 1 = C → P ⁡ A = P ⁡ A + 1 ↔ P ⁡ B = P ⁡ C
6 2fveq3 ⊢ A = B → I ⁡ F ⁡ A = I ⁡ F ⁡ B
7 1 sneqd ⊢ A = B → P ⁡ A = P ⁡ B
8 6 7 eqeq12d ⊢ A = B → I ⁡ F ⁡ A = P ⁡ A ↔ I ⁡ F ⁡ B = P ⁡ B
9 8 adantr ⊢ A = B ∧ A + 1 = C → I ⁡ F ⁡ A = P ⁡ A ↔ I ⁡ F ⁡ B = P ⁡ B
10 2 4 preq12d ⊢ A = B ∧ A + 1 = C → P ⁡ A P ⁡ A + 1 = P ⁡ B P ⁡ C
11 6 adantr ⊢ A = B ∧ A + 1 = C → I ⁡ F ⁡ A = I ⁡ F ⁡ B
12 10 11 sseq12d ⊢ A = B ∧ A + 1 = C → P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ P ⁡ B P ⁡ C ⊆ I ⁡ F ⁡ B
13 5 9 12 ifpbi123d ⊢ A = B ∧ A + 1 = C → if- P ⁡ A = P ⁡ A + 1 I ⁡ F ⁡ A = P ⁡ A P ⁡ A P ⁡ A + 1 ⊆ I ⁡ F ⁡ A ↔ if- P ⁡ B = P ⁡ C I ⁡ F ⁡ B = P ⁡ B P ⁡ B P ⁡ C ⊆ I ⁡ F ⁡ B