3pthdlem1

	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	3pthdlem1	$⊢ φ \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		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	1 2 3	3wlkdlem3	$⊢ φ \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$
6		simpr1l	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to A \neq B$
7		simpl	$⊢ (P (0) = A \land P (1) = B) \to P (0) = A$
8	7	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to P (0) = A$
9		simpr	$⊢ (P (0) = A \land P (1) = B) \to P (1) = B$
10	9	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to P (1) = B$
11	8 10	neeq12d	$⊢ ((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)$
12	11	adantr	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (0) \neq P (1) \leftrightarrow A \neq B)$
13	6 12	mpbird	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (0) \neq P (1)$
14	13	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (0 \neq 1 \to P (0) \neq P (1))$
15		simpr1r	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to A \neq C$
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	8 17	neeq12d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (0) \neq P (2) \leftrightarrow A \neq C)$
19	18	adantr	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (0) \neq P (2) \leftrightarrow A \neq C)$
20	15 19	mpbird	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (0) \neq P (2)$
21	20	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (0 \neq 2 \to P (0) \neq P (2))$
22	14 21	jca	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to ((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2)))$
23		eqid	$⊢ 1 = 1$
24	23	2a1i	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (1) = P (1) \to 1 = 1)$
25	24	necon3d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (1 \neq 1 \to P (1) \neq P (1))$
26		simpr2l	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to B \neq C$
27	10 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)$
28	27	adantr	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (1) \neq P (2) \leftrightarrow B \neq C)$
29	26 28	mpbird	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (1) \neq P (2)$
30	29	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (1 \neq 2 \to P (1) \neq P (2))$
31	25 30	jca	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2)))$
32	29	necomd	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (2) \neq P (1)$
33	32	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (2 \neq 1 \to P (2) \neq P (1))$
34		eqid	$⊢ 2 = 2$
35	34	2a1i	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (2) = P (2) \to 2 = 2)$
36	35	necon3d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (2 \neq 2 \to P (2) \neq P (2))$
37		simpr2r	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to B \neq D$
38		simpr	$⊢ (P (2) = C \land P (3) = D) \to P (3) = D$
39	38	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to P (3) = D$
40	10 39	neeq12d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (1) \neq P (3) \leftrightarrow B \neq D)$
41	40	adantr	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (1) \neq P (3) \leftrightarrow B \neq D)$
42	37 41	mpbird	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (1) \neq P (3)$
43	42	necomd	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (3) \neq P (1)$
44	43	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (3 \neq 1 \to P (3) \neq P (1))$
45		simp3	$⊢ ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D) \to C \neq D$
46	45	necomd	$⊢ ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D) \to D \neq C$
47	46	adantl	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to D \neq C$
48		simpl	$⊢ (P (3) = D \land P (2) = C) \to P (3) = D$
49		simpr	$⊢ (P (3) = D \land P (2) = C) \to P (2) = C$
50	48 49	neeq12d	$⊢ (P (3) = D \land P (2) = C) \to (P (3) \neq P (2) \leftrightarrow D \neq C)$
51	50	ancoms	$⊢ (P (2) = C \land P (3) = D) \to (P (3) \neq P (2) \leftrightarrow D \neq C)$
52	51	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (3) \neq P (2) \leftrightarrow D \neq C)$
53	52	adantr	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (P (3) \neq P (2) \leftrightarrow D \neq C)$
54	47 53	mpbird	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to P (3) \neq P (2)$
55	54	a1d	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (3 \neq 2 \to P (3) \neq P (2))$
56	44 55	jca	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2)))$
57	33 36 56	jca31	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2))))$
58	22 31 57	jca31	$⊢ (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \land ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)) \to ((((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))) \land ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2)))) \land (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2)))))$
59	5 4 58	syl2anc	$⊢ φ \to ((((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))) \land ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2)))) \land (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2)))))$
60	1	fveq2i	$⊢ \|P\| = \|⟨“ A B C D ”⟩\|$
61		s4len	$⊢ \|⟨“ A B C D ”⟩\| = 4$
62	60 61	eqtri	$⊢ \|P\| = 4$
63	62	oveq2i	$⊢ (0 ..^\|P\|) = (0 ..^4)$
64		fzo0to42pr	$⊢ (0 ..^4) = \{0, 1\} \cup \{2, 3\}$
65	63 64	eqtri	$⊢ (0 ..^\|P\|) = \{0, 1\} \cup \{2, 3\}$
66	65	raleqi	$⊢ \forall k \in (0 ..^\|P\|) ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow \forall k \in (\{0, 1\} \cup \{2, 3\}) ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2)))$
67		ralunb	$⊢ \forall k \in (\{0, 1\} \cup \{2, 3\}) ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow (\forall k \in \{0, 1\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \land \forall k \in \{2, 3\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))))$
68		c0ex	$⊢ 0 \in V$
69		1ex	$⊢ 1 \in V$
70		neeq1	$⊢ k = 0 \to (k \neq 1 \leftrightarrow 0 \neq 1)$
71		fveq2	$⊢ k = 0 \to P (k) = P (0)$
72	71	neeq1d	$⊢ k = 0 \to (P (k) \neq P (1) \leftrightarrow P (0) \neq P (1))$
73	70 72	imbi12d	$⊢ k = 0 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (0 \neq 1 \to P (0) \neq P (1)))$
74		neeq1	$⊢ k = 0 \to (k \neq 2 \leftrightarrow 0 \neq 2)$
75	71	neeq1d	$⊢ k = 0 \to (P (k) \neq P (2) \leftrightarrow P (0) \neq P (2))$
76	74 75	imbi12d	$⊢ k = 0 \to ((k \neq 2 \to P (k) \neq P (2)) \leftrightarrow (0 \neq 2 \to P (0) \neq P (2)))$
77	73 76	anbi12d	$⊢ k = 0 \to (((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow ((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))))$
78		neeq1	$⊢ k = 1 \to (k \neq 1 \leftrightarrow 1 \neq 1)$
79		fveq2	$⊢ k = 1 \to P (k) = P (1)$
80	79	neeq1d	$⊢ k = 1 \to (P (k) \neq P (1) \leftrightarrow P (1) \neq P (1))$
81	78 80	imbi12d	$⊢ k = 1 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (1 \neq 1 \to P (1) \neq P (1)))$
82		neeq1	$⊢ k = 1 \to (k \neq 2 \leftrightarrow 1 \neq 2)$
83	79	neeq1d	$⊢ k = 1 \to (P (k) \neq P (2) \leftrightarrow P (1) \neq P (2))$
84	82 83	imbi12d	$⊢ k = 1 \to ((k \neq 2 \to P (k) \neq P (2)) \leftrightarrow (1 \neq 2 \to P (1) \neq P (2)))$
85	81 84	anbi12d	$⊢ k = 1 \to (((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2))))$
86	68 69 77 85	ralpr	$⊢ \forall k \in \{0, 1\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow (((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))) \land ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2))))$
87		2ex	$⊢ 2 \in V$
88		3ex	$⊢ 3 \in V$
89		neeq1	$⊢ k = 2 \to (k \neq 1 \leftrightarrow 2 \neq 1)$
90		fveq2	$⊢ k = 2 \to P (k) = P (2)$
91	90	neeq1d	$⊢ k = 2 \to (P (k) \neq P (1) \leftrightarrow P (2) \neq P (1))$
92	89 91	imbi12d	$⊢ k = 2 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (2 \neq 1 \to P (2) \neq P (1)))$
93		neeq1	$⊢ k = 2 \to (k \neq 2 \leftrightarrow 2 \neq 2)$
94	90	neeq1d	$⊢ k = 2 \to (P (k) \neq P (2) \leftrightarrow P (2) \neq P (2))$
95	93 94	imbi12d	$⊢ k = 2 \to ((k \neq 2 \to P (k) \neq P (2)) \leftrightarrow (2 \neq 2 \to P (2) \neq P (2)))$
96	92 95	anbi12d	$⊢ k = 2 \to (((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow ((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))))$
97		neeq1	$⊢ k = 3 \to (k \neq 1 \leftrightarrow 3 \neq 1)$
98		fveq2	$⊢ k = 3 \to P (k) = P (3)$
99	98	neeq1d	$⊢ k = 3 \to (P (k) \neq P (1) \leftrightarrow P (3) \neq P (1))$
100	97 99	imbi12d	$⊢ k = 3 \to ((k \neq 1 \to P (k) \neq P (1)) \leftrightarrow (3 \neq 1 \to P (3) \neq P (1)))$
101		neeq1	$⊢ k = 3 \to (k \neq 2 \leftrightarrow 3 \neq 2)$
102	98	neeq1d	$⊢ k = 3 \to (P (k) \neq P (2) \leftrightarrow P (3) \neq P (2))$
103	101 102	imbi12d	$⊢ k = 3 \to ((k \neq 2 \to P (k) \neq P (2)) \leftrightarrow (3 \neq 2 \to P (3) \neq P (2)))$
104	100 103	anbi12d	$⊢ k = 3 \to (((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2))))$
105	87 88 96 104	ralpr	$⊢ \forall k \in \{2, 3\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2))))$
106	86 105	anbi12i	$⊢ (\forall k \in \{0, 1\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \land \forall k \in \{2, 3\} ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2)))) \leftrightarrow ((((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))) \land ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2)))) \land (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2)))))$
107	66 67 106	3bitri	$⊢ \forall k \in (0 ..^\|P\|) ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2))) \leftrightarrow ((((0 \neq 1 \to P (0) \neq P (1)) \land (0 \neq 2 \to P (0) \neq P (2))) \land ((1 \neq 1 \to P (1) \neq P (1)) \land (1 \neq 2 \to P (1) \neq P (2)))) \land (((2 \neq 1 \to P (2) \neq P (1)) \land (2 \neq 2 \to P (2) \neq P (2))) \land ((3 \neq 1 \to P (3) \neq P (1)) \land (3 \neq 2 \to P (3) \neq P (2)))))$
108	59 107	sylibr	$⊢ φ \to \forall k \in (0 ..^\|P\|) ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2)))$
109	2	fveq2i	$⊢ \|F\| = \|⟨“ J K L ”⟩\|$
110		s3len	$⊢ \|⟨“ J K L ”⟩\| = 3$
111	109 110	eqtri	$⊢ \|F\| = 3$
112	111	oveq2i	$⊢ (1 ..^\|F\|) = (1 ..^3)$
113		fzo13pr	$⊢ (1 ..^3) = \{1, 2\}$
114	112 113	eqtri	$⊢ (1 ..^\|F\|) = \{1, 2\}$
115	114	raleqi	$⊢ \forall j \in (1 ..^\|F\|) (k \neq j \to P (k) \neq P (j)) \leftrightarrow \forall j \in \{1, 2\} (k \neq j \to P (k) \neq P (j))$
116		neeq2	$⊢ j = 1 \to (k \neq j \leftrightarrow k \neq 1)$
117		fveq2	$⊢ j = 1 \to P (j) = P (1)$
118	117	neeq2d	$⊢ j = 1 \to (P (k) \neq P (j) \leftrightarrow P (k) \neq P (1))$
119	116 118	imbi12d	$⊢ j = 1 \to ((k \neq j \to P (k) \neq P (j)) \leftrightarrow (k \neq 1 \to P (k) \neq P (1)))$
120		neeq2	$⊢ j = 2 \to (k \neq j \leftrightarrow k \neq 2)$
121		fveq2	$⊢ j = 2 \to P (j) = P (2)$
122	121	neeq2d	$⊢ j = 2 \to (P (k) \neq P (j) \leftrightarrow P (k) \neq P (2))$
123	120 122	imbi12d	$⊢ j = 2 \to ((k \neq j \to P (k) \neq P (j)) \leftrightarrow (k \neq 2 \to P (k) \neq P (2)))$
124	69 87 119 123	ralpr	$⊢ \forall j \in \{1, 2\} (k \neq j \to P (k) \neq P (j)) \leftrightarrow ((k \neq 1 \to P (k) \neq P (1)) \land (k \neq 2 \to P (k) \neq P (2)))$
125	115 124	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)) \land (k \neq 2 \to P (k) \neq P (2)))$
126	125	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)) \land (k \neq 2 \to P (k) \neq P (2)))$
127	108 126	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 3pthdlem1

Proof