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..^FP⁡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=01
16 15 raleqi ⊢∀k∈0..^FP⁡k≠P⁡k+1↔∀k∈01P⁡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∈01P⁡k≠P⁡k+1↔P⁡0≠P⁡1∧P⁡1≠P⁡2
29 16 28 bitri ⊢∀k∈0..^FP⁡k≠P⁡k+1↔P⁡0≠P⁡1∧P⁡1≠P⁡2
30 14 29 sylibr ⊢φ→∀k∈0..^FP⁡k≠P⁡k+1