Metamath Proof Explorer

Theorem 2wlkdlem5

Description: Lemma 5 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p ⊢ P = ⟨“ ABC ”⟩
2wlkd.f ⊢ F = ⟨“ JK ”⟩
2wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
2wlkd.n ⊢ φ → A ≠ B ∧ B ≠ C
Assertion 2wlkdlem5 ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ P = ⟨“ ABC ”⟩
2 2wlkd.f ⊢ F = ⟨“ JK ”⟩
3 2wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V
4 2wlkd.n ⊢ φ → A ≠ B ∧ B ≠ C
5 1 2 3 2wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C
6 simp1 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 = A
7 simp2 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 = B
8 6 7 neeq12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 ≠ P ⁡ 1 ↔ A ≠ B
9 simp3 ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 2 = C
10 7 9 neeq12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 1 ≠ P ⁡ 2 ↔ B ≠ C
11 8 10 anbi12d ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2 ↔ A ≠ B ∧ B ≠ C
12 11 bicomd ⊢ P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C → A ≠ B ∧ B ≠ C ↔ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2
13 5 12 syl ⊢ φ → A ≠ B ∧ B ≠ C ↔ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2
14 4 13 mpbid ⊢ φ → P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2
15 1 2 2wlkdlem2 ⊢ 0 ..^ F = 0 1
16 15 raleqi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ↔ ∀ k ∈ 0 1 P ⁡ k ≠ P ⁡ k + 1
17 c0ex ⊢ 0 ∈ V
18 1ex ⊢ 1 ∈ V
19 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
20 fv0p1e1 ⊢ k = 0 → P ⁡ k + 1 = P ⁡ 1
21 19 20 neeq12d ⊢ k = 0 → P ⁡ k ≠ P ⁡ k + 1 ↔ P ⁡ 0 ≠ P ⁡ 1
22 fveq2 ⊢ k = 1 → P ⁡ k = P ⁡ 1
23 oveq1 ⊢ k = 1 → k + 1 = 1 + 1
24 1p1e2 ⊢ 1 + 1 = 2
25 23 24 eqtrdi ⊢ k = 1 → k + 1 = 2
26 25 fveq2d ⊢ k = 1 → P ⁡ k + 1 = P ⁡ 2
27 22 26 neeq12d ⊢ k = 1 → P ⁡ k ≠ P ⁡ k + 1 ↔ P ⁡ 1 ≠ P ⁡ 2
28 17 18 21 27 ralpr ⊢ ∀ k ∈ 0 1 P ⁡ k ≠ P ⁡ k + 1 ↔ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2
29 16 28 bitri ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ↔ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 1 ≠ P ⁡ 2
30 14 29 sylibr ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1