3wlkdlem5

	Ref	Expression
Hypotheses	3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
	3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
	3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
	3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
Assertion	3wlkdlem5	$⊢ φ \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
2		3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
3		3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
4		3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
5		simpl	$⊢ (A \neq B \land A \neq C) \to A \neq B$
6		simpl	$⊢ (B \neq C \land B \neq D) \to B \neq C$
7		id	$⊢ C \neq D \to C \neq D$
8	5 6 7	3anim123i	$⊢ ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D) \to (A \neq B \land B \neq C \land C \neq D)$
9	4 8	syl	$⊢ φ \to (A \neq B \land B \neq C \land C \neq D)$
10	1 2 3	3wlkdlem3	$⊢ φ \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$
11		simpl	$⊢ (P (0) = A \land P (1) = B) \to P (0) = A$
12		simpr	$⊢ (P (0) = A \land P (1) = B) \to P (1) = B$
13	11 12	neeq12d	$⊢ (P (0) = A \land P (1) = B) \to (P (0) \neq P (1) \leftrightarrow A \neq B)$
14	13	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (0) \neq P (1) \leftrightarrow A \neq B)$
15	12	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to P (1) = B$
16		simpl	$⊢ (P (2) = C \land P (3) = D) \to P (2) = C$
17	16	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to P (2) = C$
18	15 17	neeq12d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (1) \neq P (2) \leftrightarrow B \neq C)$
19		simpr	$⊢ (P (2) = C \land P (3) = D) \to P (3) = D$
20	16 19	neeq12d	$⊢ (P (2) = C \land P (3) = D) \to (P (2) \neq P (3) \leftrightarrow C \neq D)$
21	20	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (2) \neq P (3) \leftrightarrow C \neq D)$
22	14 18 21	3anbi123d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to ((P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (3)) \leftrightarrow (A \neq B \land B \neq C \land C \neq D))$
23	10 22	syl	$⊢ φ \to ((P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (3)) \leftrightarrow (A \neq B \land B \neq C \land C \neq D))$
24	9 23	mpbird	$⊢ φ \to (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (3))$
25	1 2	3wlkdlem2	$⊢ (0 ..^\|F\|) = \{0, 1, 2\}$
26	25	raleqi	$⊢ \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1) \leftrightarrow \forall k \in \{0, 1, 2\} P (k) \neq P (k + 1)$
27		c0ex	$⊢ 0 \in V$
28		1ex	$⊢ 1 \in V$
29		2ex	$⊢ 2 \in V$
30		fveq2	$⊢ k = 0 \to P (k) = P (0)$
31		fv0p1e1	$⊢ k = 0 \to P (k + 1) = P (1)$
32	30 31	neeq12d	$⊢ k = 0 \to (P (k) \neq P (k + 1) \leftrightarrow P (0) \neq P (1))$
33		fveq2	$⊢ k = 1 \to P (k) = P (1)$
34		oveq1	$⊢ k = 1 \to k + 1 = 1 + 1$
35		1p1e2	$⊢ 1 + 1 = 2$
36	34 35	eqtrdi	$⊢ k = 1 \to k + 1 = 2$
37	36	fveq2d	$⊢ k = 1 \to P (k + 1) = P (2)$
38	33 37	neeq12d	$⊢ k = 1 \to (P (k) \neq P (k + 1) \leftrightarrow P (1) \neq P (2))$
39		fveq2	$⊢ k = 2 \to P (k) = P (2)$
40		oveq1	$⊢ k = 2 \to k + 1 = 2 + 1$
41		2p1e3	$⊢ 2 + 1 = 3$
42	40 41	eqtrdi	$⊢ k = 2 \to k + 1 = 3$
43	42	fveq2d	$⊢ k = 2 \to P (k + 1) = P (3)$
44	39 43	neeq12d	$⊢ k = 2 \to (P (k) \neq P (k + 1) \leftrightarrow P (2) \neq P (3))$
45	27 28 29 32 38 44	raltp	$⊢ \forall k \in \{0, 1, 2\} P (k) \neq P (k + 1) \leftrightarrow (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (3))$
46	26 45	bitri	$⊢ \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1) \leftrightarrow (P (0) \neq P (1) \land P (1) \neq P (2) \land P (2) \neq P (3))$
47	24 46	sylibr	$⊢ φ \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$

Metamath Proof Explorer

Theorem 3wlkdlem5

Proof