Metamath Proof Explorer

Theorem 3wlkdlem5

Description: Lemma 5 for 3wlkd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 7-Feb-2021)

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

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢P=⟨“ABCD”⟩
2 3wlkd.f ⊢F=⟨“JKL”⟩
3 3wlkd.s ⊢φ→A∈V∧B∈V∧C∈V∧D∈V
4 3wlkd.n ⊢φ→A≠B∧A≠C∧B≠C∧B≠D∧C≠D
5 simpl ⊢A≠B∧A≠C→A≠B
6 simpl ⊢B≠C∧B≠D→B≠C
7 id ⊢C≠D→C≠D
8 5 6 7 3anim123i ⊢A≠B∧A≠C∧B≠C∧B≠D∧C≠D→A≠B∧B≠C∧C≠D
9 4 8 syl ⊢φ→A≠B∧B≠C∧C≠D
10 1 2 3 3wlkdlem3 ⊢φ→P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D
11 simpl ⊢P⁡0=A∧P⁡1=B→P⁡0=A
12 simpr ⊢P⁡0=A∧P⁡1=B→P⁡1=B
13 11 12 neeq12d ⊢P⁡0=A∧P⁡1=B→P⁡0≠P⁡1↔A≠B
14 13 adantr ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡0≠P⁡1↔A≠B
15 12 adantr ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡1=B
16 simpl ⊢P⁡2=C∧P⁡3=D→P⁡2=C
17 16 adantl ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡2=C
18 15 17 neeq12d ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡1≠P⁡2↔B≠C
19 simpr ⊢P⁡2=C∧P⁡3=D→P⁡3=D
20 16 19 neeq12d ⊢P⁡2=C∧P⁡3=D→P⁡2≠P⁡3↔C≠D
21 20 adantl ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡2≠P⁡3↔C≠D
22 14 18 21 3anbi123d ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡0≠P⁡1∧P⁡1≠P⁡2∧P⁡2≠P⁡3↔A≠B∧B≠C∧C≠D
23 10 22 syl ⊢φ→P⁡0≠P⁡1∧P⁡1≠P⁡2∧P⁡2≠P⁡3↔A≠B∧B≠C∧C≠D
24 9 23 mpbird ⊢φ→P⁡0≠P⁡1∧P⁡1≠P⁡2∧P⁡2≠P⁡3
25 1 2 3wlkdlem2 ⊢0..^F=012
26 25 raleqi ⊢∀k∈0..^FP⁡k≠P⁡k+1↔∀k∈012P⁡k≠P⁡k+1
27 c0ex ⊢0∈V
28 1ex ⊢1∈V
29 2ex ⊢2∈V
30 fveq2 ⊢k=0→P⁡k=P⁡0
31 fv0p1e1 ⊢k=0→P⁡k+1=P⁡1
32 30 31 neeq12d ⊢k=0→P⁡k≠P⁡k+1↔P⁡0≠P⁡1
33 fveq2 ⊢k=1→P⁡k=P⁡1
34 oveq1 ⊢k=1→k+1=1+1
35 1p1e2 ⊢1+1=2
36 34 35 eqtrdi ⊢k=1→k+1=2
37 36 fveq2d ⊢k=1→P⁡k+1=P⁡2
38 33 37 neeq12d ⊢k=1→P⁡k≠P⁡k+1↔P⁡1≠P⁡2
39 fveq2 ⊢k=2→P⁡k=P⁡2
40 oveq1 ⊢k=2→k+1=2+1
41 2p1e3 ⊢2+1=3
42 40 41 eqtrdi ⊢k=2→k+1=3
43 42 fveq2d ⊢k=2→P⁡k+1=P⁡3
44 39 43 neeq12d ⊢k=2→P⁡k≠P⁡k+1↔P⁡2≠P⁡3
45 27 28 29 32 38 44 raltp ⊢∀k∈012P⁡k≠P⁡k+1↔P⁡0≠P⁡1∧P⁡1≠P⁡2∧P⁡2≠P⁡3
46 26 45 bitri ⊢∀k∈0..^FP⁡k≠P⁡k+1↔P⁡0≠P⁡1∧P⁡1≠P⁡2∧P⁡2≠P⁡3
47 24 46 sylibr ⊢φ→∀k∈0..^FP⁡k≠P⁡k+1