2pthdlem1

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

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
2		2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
3		2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
4		2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
5	1 2 3	2wlkdlem3	$⊢ φ \to (P (0) = A \land P (1) = B \land P (2) = C)$
6		simpl	$⊢ (P (0) = A \land P (1) = B) \to P (0) = A$
7		simpr	$⊢ (P (0) = A \land P (1) = B) \to P (1) = B$
8	6 7	neeq12d	$⊢ (P (0) = A \land P (1) = B) \to (P (0) \neq P (1) \leftrightarrow A \neq B)$
9	8	bicomd	$⊢ (P (0) = A \land P (1) = B) \to (A \neq B \leftrightarrow P (0) \neq P (1))$
10	9	3adant3	$⊢ (P (0) = A \land P (1) = B \land P (2) = C) \to (A \neq B \leftrightarrow P (0) \neq P (1))$
11	10	biimpcd	$⊢ A \neq B \to ((P (0) = A \land P (1) = B \land P (2) = C) \to P (0) \neq P (1))$
12	11	adantr	$⊢ (A \neq B \land B \neq C) \to ((P (0) = A \land P (1) = B \land P (2) = C) \to P (0) \neq P (1))$
13	12	imp	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to P (0) \neq P (1)$
14	13	a1d	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to (0 \neq 1 \to P (0) \neq P (1))$
15		eqid	$⊢ 1 = 1$
16		eqneqall	$⊢ 1 = 1 \to (1 \neq 1 \to P (1) \neq P (1))$
17	15 16	mp1i	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to (1 \neq 1 \to P (1) \neq P (1))$
18		simpr	$⊢ (P (1) = B \land P (2) = C) \to P (2) = C$
19		simpl	$⊢ (P (1) = B \land P (2) = C) \to P (1) = B$
20	18 19	neeq12d	$⊢ (P (1) = B \land P (2) = C) \to (P (2) \neq P (1) \leftrightarrow C \neq B)$
21		necom	$⊢ C \neq B \leftrightarrow B \neq C$
22	20 21	bitr2di	$⊢ (P (1) = B \land P (2) = C) \to (B \neq C \leftrightarrow P (2) \neq P (1))$
23	22	3adant1	$⊢ (P (0) = A \land P (1) = B \land P (2) = C) \to (B \neq C \leftrightarrow P (2) \neq P (1))$
24	23	biimpcd	$⊢ B \neq C \to ((P (0) = A \land P (1) = B \land P (2) = C) \to P (2) \neq P (1))$
25	24	adantl	$⊢ (A \neq B \land B \neq C) \to ((P (0) = A \land P (1) = B \land P (2) = C) \to P (2) \neq P (1))$
26	25	imp	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to P (2) \neq P (1)$
27	26	a1d	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to (2 \neq 1 \to P (2) \neq P (1))$
28	14 17 27	3jca	$⊢ ((A \neq B \land B \neq C) \land (P (0) = A \land P (1) = B \land P (2) = C)) \to ((0 \neq 1 \to P (0) \neq P (1)) \land (1 \neq 1 \to P (1) \neq P (1)) \land (2 \neq 1 \to P (2) \neq P (1)))$
29	4 5 28	syl2anc	$⊢ φ \to ((0 \neq 1 \to P (0) \neq P (1)) \land (1 \neq 1 \to P (1) \neq P (1)) \land (2 \neq 1 \to P (2) \neq P (1)))$
30	1	fveq2i	$⊢ \|P\| = \|⟨“ A B C ”⟩\|$
31		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
32	30 31	eqtri	$⊢ \|P\| = 3$
33	32	oveq2i	$⊢ (0 ..^\|P\|) = (0 ..^3)$
34		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
35	33 34	eqtri	$⊢ (0 ..^\|P\|) = \{0, 1, 2\}$
36	35	raleqi	$⊢ \forall k \in (0 ..^\|P\|) (k \neq 1 \to P (k) \neq P (1)) \leftrightarrow \forall k \in \{0, 1, 2\} (k \neq 1 \to P (k) \neq P (1))$
37		c0ex	$⊢ 0 \in V$
38		1ex	$⊢ 1 \in V$
39		2ex	$⊢ 2 \in V$
40		neeq1	$⊢ k = 0 \to (k \neq 1 \leftrightarrow 0 \neq 1)$
41		fveq2	$⊢ k = 0 \to P (k) = P (0)$
42	41	neeq1d	$⊢ k = 0 \to (P (k) \neq P (1) \leftrightarrow P (0) \neq P (1))$
43	40 42	imbi12d	$⊢ k = 0 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (0 \neq 1 \to P (0) \neq P (1)))$
44		neeq1	$⊢ k = 1 \to (k \neq 1 \leftrightarrow 1 \neq 1)$
45		fveq2	$⊢ k = 1 \to P (k) = P (1)$
46	45	neeq1d	$⊢ k = 1 \to (P (k) \neq P (1) \leftrightarrow P (1) \neq P (1))$
47	44 46	imbi12d	$⊢ k = 1 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (1 \neq 1 \to P (1) \neq P (1)))$
48		neeq1	$⊢ k = 2 \to (k \neq 1 \leftrightarrow 2 \neq 1)$
49		fveq2	$⊢ k = 2 \to P (k) = P (2)$
50	49	neeq1d	$⊢ k = 2 \to (P (k) \neq P (1) \leftrightarrow P (2) \neq P (1))$
51	48 50	imbi12d	$⊢ k = 2 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (2 \neq 1 \to P (2) \neq P (1)))$
52	37 38 39 43 47 51	raltp	$⊢ \forall k \in \{0, 1, 2\} (k \neq 1 \to P (k) \neq P (1)) \leftrightarrow ((0 \neq 1 \to P (0) \neq P (1)) \land (1 \neq 1 \to P (1) \neq P (1)) \land (2 \neq 1 \to P (2) \neq P (1)))$
53	36 52	bitri	$⊢ \forall k \in (0 ..^\|P\|) (k \neq 1 \to P (k) \neq P (1)) \leftrightarrow ((0 \neq 1 \to P (0) \neq P (1)) \land (1 \neq 1 \to P (1) \neq P (1)) \land (2 \neq 1 \to P (2) \neq P (1)))$
54	29 53	sylibr	$⊢ φ \to \forall k \in (0 ..^\|P\|) (k \neq 1 \to P (k) \neq P (1))$
55	2	fveq2i	$⊢ \|F\| = \|⟨“ J K ”⟩\|$
56		s2len	$⊢ \|⟨“ J K ”⟩\| = 2$
57	55 56	eqtri	$⊢ \|F\| = 2$
58	57	oveq2i	$⊢ (1 ..^\|F\|) = (1 ..^2)$
59		fzo12sn	$⊢ (1 ..^2) = \{1\}$
60	58 59	eqtri	$⊢ (1 ..^\|F\|) = \{1\}$
61	60	raleqi	$⊢ \forall j \in (1 ..^\|F\|) (k \neq j \to P (k) \neq P (j)) \leftrightarrow \forall j \in \{1\} (k \neq j \to P (k) \neq P (j))$
62		neeq2	$⊢ j = 1 \to (k \neq j \leftrightarrow k \neq 1)$
63		fveq2	$⊢ j = 1 \to P (j) = P (1)$
64	63	neeq2d	$⊢ j = 1 \to (P (k) \neq P (j) \leftrightarrow P (k) \neq P (1))$
65	62 64	imbi12d	$⊢ j = 1 \to ((k \neq j \to P (k) \neq P (j)) \leftrightarrow (k \neq 1 \to P (k) \neq P (1)))$
66	38 65	ralsn	$⊢ \forall j \in \{1\} (k \neq j \to P (k) \neq P (j)) \leftrightarrow (k \neq 1 \to P (k) \neq P (1))$
67	61 66	bitri	$⊢ \forall j \in (1 ..^\|F\|) (k \neq j \to P (k) \neq P (j)) \leftrightarrow (k \neq 1 \to P (k) \neq P (1))$
68	67	ralbii	$⊢ \forall k \in (0 ..^\|P\|) \forall j \in (1 ..^\|F\|) (k \neq j \to P (k) \neq P (j)) \leftrightarrow \forall k \in (0 ..^\|P\|) (k \neq 1 \to P (k) \neq P (1))$
69	54 68	sylibr	$⊢ φ \to \forall k \in (0 ..^\|P\|) \forall j \in (1 ..^\|F\|) (k \neq j \to P (k) \neq P (j))$

Metamath Proof Explorer

Theorem 2pthdlem1

Proof