Metamath Proof Explorer

Theorem 2wlkdlem5

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

Ref Expression
Hypotheses 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
Assertion 2wlkdlem5 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4 2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
5 1 2 3 2wlkdlem3 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )
6 simp1 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
7 simp2 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 1 ) = 𝐵 )
8 6 7 neeq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ↔ 𝐴 ≠ 𝐵 ) )
9 simp3 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 2 ) = 𝐶 )
10 7 9 neeq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ↔ 𝐵 ≠ 𝐶 ) )
11 8 10 anbi12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
12 11 bicomd ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
13 5 12 syl ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) ) )
14 4 13 mpbid ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
15 1 2 2wlkdlem2 ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 }
16 15 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
17 c0ex ⊢ 0 ∈ V
18 1ex ⊢ 1 ∈ V
19 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
20 fv0p1e1 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
21 19 20 neeq12d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
22 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
23 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
24 1p1e2 ⊢ ( 1 + 1 ) = 2
25 23 24 eqtrdi ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = 2 )
26 25 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 2 ) )
27 22 26 neeq12d ⊢ ( 𝑘 = 1 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
28 17 18 21 27 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
29 16 28 bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ∧ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 2 ) ) )
30 14 29 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )