axlowdim

Description: The general lower dimension axiom. Take a dimension N greater than or equal to three. Then, there are three non-colinear points in N dimensional space that are equidistant from N - 1 distinct points. Derived from remarks inTarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013)

		Ref	Expression
	Assertion	axlowdim	$⊢ N \in ℤ_{\geq 3} \to \exists p \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩))$

Proof

Step	Hyp	Ref	Expression
1		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
2		0re	$⊢ 0 \in ℝ$
3	2 2	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
4	1 3	syl	$⊢ N \in ℤ_{\geq 3} \to \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
5		1re	$⊢ 1 \in ℝ$
6	5 2	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
7	1 6	syl	$⊢ N \in ℤ_{\geq 3} \to \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
8	2 5	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
9	1 8	syl	$⊢ N \in ℤ_{\geq 3} \to \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
10		eqid	$⊢ (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})))$
11	10	axlowdimlem15	$⊢ N \in ℤ_{\geq 3} \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N)$
12		eqid	$⊢ \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
13		eqid	$⊢ \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) = \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})$
14		eqid	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
15	12 13 14 2 2	axlowdimlem17	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
16		eqid	$⊢ \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
17	12 13 16 5 2	axlowdimlem17	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
18		eqid	$⊢ \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})$
19	12 13 18 2 5	axlowdimlem17	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
20		1zzd	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 1 \in ℤ$
21		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
22	21	3ad2ant2	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to N - 1 \in ℤ$
23		2m1e1	$⊢ 2 - 1 = 1$
24		2re	$⊢ 2 \in ℝ$
25		3re	$⊢ 3 \in ℝ$
26		2lt3	$⊢ 2 < 3$
27	24 25 26	ltleii	$⊢ 2 \leq 3$
28		zre	$⊢ N \in ℤ \to N \in ℝ$
29		letr	$⊢ (2 \in ℝ \land 3 \in ℝ \land N \in ℝ) \to ((2 \leq 3 \land 3 \leq N) \to 2 \leq N)$
30	24 25 28 29	mp3an12i	$⊢ N \in ℤ \to ((2 \leq 3 \land 3 \leq N) \to 2 \leq N)$
31	27 30	mpani	$⊢ N \in ℤ \to (3 \leq N \to 2 \leq N)$
32	31	imp	$⊢ (N \in ℤ \land 3 \leq N) \to 2 \leq N$
33	32	3adant1	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 2 \leq N$
34	28	3ad2ant2	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to N \in ℝ$
35		lesub1	$⊢ (2 \in ℝ \land N \in ℝ \land 1 \in ℝ) \to (2 \leq N \leftrightarrow 2 - 1 \leq N - 1)$
36	24 5 35	mp3an13	$⊢ N \in ℝ \to (2 \leq N \leftrightarrow 2 - 1 \leq N - 1)$
37	34 36	syl	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to (2 \leq N \leftrightarrow 2 - 1 \leq N - 1)$
38	33 37	mpbid	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 2 - 1 \leq N - 1$
39	23 38	eqbrtrrid	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to 1 \leq N - 1$
40	20 22 39	3jca	$⊢ (3 \in ℤ \land N \in ℤ \land 3 \leq N) \to (1 \in ℤ \land N - 1 \in ℤ \land 1 \leq N - 1)$
41		eluz2	$⊢ N \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land N \in ℤ \land 3 \leq N)$
42		eluz2	$⊢ N - 1 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land N - 1 \in ℤ \land 1 \leq N - 1)$
43	40 41 42	3imtr4i	$⊢ N \in ℤ_{\geq 3} \to N - 1 \in ℤ_{\geq 1}$
44		eluzfz1	$⊢ N - 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots N - 1)$
45	43 44	syl	$⊢ N \in ℤ_{\geq 3} \to 1 \in (1 \dots N - 1)$
46	45	adantr	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to 1 \in (1 \dots N - 1)$
47		eqeq1	$⊢ k = 1 \to (k = 1 \leftrightarrow 1 = 1)$
48		oveq1	$⊢ k = 1 \to k + 1 = 1 + 1$
49	48	opeq1d	$⊢ k = 1 \to ⟨k + 1, 1⟩ = ⟨1 + 1, 1⟩$
50	49	sneqd	$⊢ k = 1 \to \{⟨k + 1, 1⟩\} = \{⟨1 + 1, 1⟩\}$
51	48	sneqd	$⊢ k = 1 \to \{k + 1\} = \{1 + 1\}$
52	51	difeq2d	$⊢ k = 1 \to (1 \dots N) ∖ \{k + 1\} = (1 \dots N) ∖ \{1 + 1\}$
53	52	xpeq1d	$⊢ k = 1 \to ((1 \dots N) ∖ \{k + 1\}) \times \{0\} = ((1 \dots N) ∖ \{1 + 1\}) \times \{0\}$
54	50 53	uneq12d	$⊢ k = 1 \to \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) = \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\})$
55	47 54	ifbieq2d	$⊢ k = 1 \to if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) = if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\}))$
56		snex	$⊢ \{⟨3, - 1⟩\} \in V$
57		ovex	$⊢ (1 \dots N) \in V$
58	57	difexi	$⊢ (1 \dots N) ∖ \{3\} \in V$
59		snex	$⊢ \{0\} \in V$
60	58 59	xpex	$⊢ ((1 \dots N) ∖ \{3\}) \times \{0\} \in V$
61	56 60	unex	$⊢ \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \in V$
62		snex	$⊢ \{⟨1 + 1, 1⟩\} \in V$
63	57	difexi	$⊢ (1 \dots N) ∖ \{1 + 1\} \in V$
64	63 59	xpex	$⊢ ((1 \dots N) ∖ \{1 + 1\}) \times \{0\} \in V$
65	62 64	unex	$⊢ \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\}) \in V$
66	61 65	ifex	$⊢ if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\})) \in V$
67	55 10 66	fvmpt	$⊢ 1 \in (1 \dots N - 1) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1) = if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\}))$
68	46 67	syl	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1) = if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\}))$
69		eqid	$⊢ 1 = 1$
70	69	iftruei	$⊢ if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\})) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
71	68 70	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
72	71	opeq1d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
73		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
74		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N - 1) \subseteq (1 \dots N - 1)$
75	73 74	ax-mp	$⊢ (2 \dots N - 1) \subseteq (1 \dots N - 1)$
76	75	sseli	$⊢ i \in (2 \dots N - 1) \to i \in (1 \dots N - 1)$
77	76	adantl	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to i \in (1 \dots N - 1)$
78		eqeq1	$⊢ k = i \to (k = 1 \leftrightarrow i = 1)$
79		oveq1	$⊢ k = i \to k + 1 = i + 1$
80	79	opeq1d	$⊢ k = i \to ⟨k + 1, 1⟩ = ⟨i + 1, 1⟩$
81	80	sneqd	$⊢ k = i \to \{⟨k + 1, 1⟩\} = \{⟨i + 1, 1⟩\}$
82	79	sneqd	$⊢ k = i \to \{k + 1\} = \{i + 1\}$
83	82	difeq2d	$⊢ k = i \to (1 \dots N) ∖ \{k + 1\} = (1 \dots N) ∖ \{i + 1\}$
84	83	xpeq1d	$⊢ k = i \to ((1 \dots N) ∖ \{k + 1\}) \times \{0\} = ((1 \dots N) ∖ \{i + 1\}) \times \{0\}$
85	81 84	uneq12d	$⊢ k = i \to \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) = \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})$
86	78 85	ifbieq2d	$⊢ k = i \to if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) = if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}))$
87		snex	$⊢ \{⟨i + 1, 1⟩\} \in V$
88	57	difexi	$⊢ (1 \dots N) ∖ \{i + 1\} \in V$
89	88 59	xpex	$⊢ ((1 \dots N) ∖ \{i + 1\}) \times \{0\} \in V$
90	87 89	unex	$⊢ \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) \in V$
91	61 90	ifex	$⊢ if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})) \in V$
92	86 10 91	fvmpt	$⊢ i \in (1 \dots N - 1) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i) = if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}))$
93	77 92	syl	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i) = if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}))$
94		1lt2	$⊢ 1 < 2$
95	5 24	ltnlei	$⊢ 1 < 2 \leftrightarrow \neg 2 \leq 1$
96	94 95	mpbi	$⊢ \neg 2 \leq 1$
97	96	intnanr	$⊢ \neg (2 \leq 1 \land 1 \leq N - 1)$
98		1z	$⊢ 1 \in ℤ$
99		2z	$⊢ 2 \in ℤ$
100		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
101	100 21	syl	$⊢ N \in ℤ_{\geq 3} \to N - 1 \in ℤ$
102		elfz	$⊢ (1 \in ℤ \land 2 \in ℤ \land N - 1 \in ℤ) \to (1 \in (2 \dots N - 1) \leftrightarrow (2 \leq 1 \land 1 \leq N - 1))$
103	98 99 101 102	mp3an12i	$⊢ N \in ℤ_{\geq 3} \to (1 \in (2 \dots N - 1) \leftrightarrow (2 \leq 1 \land 1 \leq N - 1))$
104	97 103	mtbiri	$⊢ N \in ℤ_{\geq 3} \to \neg 1 \in (2 \dots N - 1)$
105		eleq1	$⊢ i = 1 \to (i \in (2 \dots N - 1) \leftrightarrow 1 \in (2 \dots N - 1))$
106	105	notbid	$⊢ i = 1 \to (\neg i \in (2 \dots N - 1) \leftrightarrow \neg 1 \in (2 \dots N - 1))$
107	104 106	syl5ibrcom	$⊢ N \in ℤ_{\geq 3} \to (i = 1 \to \neg i \in (2 \dots N - 1))$
108	107	con2d	$⊢ N \in ℤ_{\geq 3} \to (i \in (2 \dots N - 1) \to \neg i = 1)$
109	108	imp	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to \neg i = 1$
110	109	iffalsed	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})) = \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})$
111	93 110	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i) = \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})$
112	111	opeq1d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
113	72 112	breq12d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
114	71	opeq1d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
115	111	opeq1d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
116	114 115	breq12d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
117	45 67	syl	$⊢ N \in ℤ_{\geq 3} \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1) = if (1 = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1 + 1, 1⟩\} \cup (((1 \dots N) ∖ \{1 + 1\}) \times \{0\}))$
118	117 70	eqtrdi	$⊢ N \in ℤ_{\geq 3} \to (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
119	118	opeq1d	$⊢ N \in ℤ_{\geq 3} \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
120	119	adantr	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
121	111	opeq1d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
122	120 121	breq12d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
123	113 116 122	3anbi123d	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to ((⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow (⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨\{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
124	15 17 19 123	mpbir3and	$⊢ (N \in ℤ_{\geq 3} \land i \in (2 \dots N - 1)) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
125	124	ralrimiva	$⊢ N \in ℤ_{\geq 3} \to \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
126	14 16 18	axlowdimlem6	$⊢ N \in ℤ_{\geq 2} \to \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
127	1 126	syl	$⊢ N \in ℤ_{\geq 3} \to \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
128		opeq2	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
129		opeq2	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
130	128 129	breq12d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
131	130	3anbi1d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
132	131	ralbidv	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
133		breq1	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (x Btwn ⟨y, z⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩)$
134		opeq2	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨z, x⟩ = ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
135	134	breq2d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (y Btwn ⟨z, x⟩ \leftrightarrow y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
136		opeq1	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨x, y⟩ = ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩$
137	136	breq2d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨x, y⟩ \leftrightarrow z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩)$
138	133 135 137	3orbi123d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩))$
139	138	notbid	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩) \leftrightarrow \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩))$
140	132 139	3anbi23d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)) \leftrightarrow ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩)))$
141		opeq2	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
142		opeq2	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
143	141 142	breq12d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
144	143	3anbi2d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
145	144	ralbidv	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
146		opeq1	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨y, z⟩ = ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩$
147	146	breq2d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩)$
148		breq1	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
149		opeq2	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩ = ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
150	149	breq2d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩ \leftrightarrow z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
151	147 148 150	3orbi123d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
152	151	notbid	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩) \leftrightarrow \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
153	145 152	3anbi23d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩)) \leftrightarrow ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)))$
154		opeq2	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
155		opeq2	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
156	154 155	breq12d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
157	156	3anbi3d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ((⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
158	157	ralbidv	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (\forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \leftrightarrow \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
159		opeq2	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ = ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
160	159	breq2d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
161		opeq1	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
162	161	breq2d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
163		breq1	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
164	160 162 163	3orbi123d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
165	164	notbid	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
166	158 165	3anbi23d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)) \leftrightarrow ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)))$
167	140 153 166	rspc3ev	$⊢ ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \land \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \land \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)) \land ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩) \land \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩))$
168	4 7 9 11 125 127 167	syl33anc	$⊢ N \in ℤ_{\geq 3} \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩))$
169		ovex	$⊢ (1 \dots N - 1) \in V$
170	169	mptex	$⊢ (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \in V$
171		f1eq1	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \leftrightarrow (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N))$
172		fveq1	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to p (1) = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1)$
173	172	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (1), x⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩$
174		fveq1	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to p (i) = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i)$
175	174	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (i), x⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩$
176	173 175	breq12d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩)$
177	172	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (1), y⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩$
178	174	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (i), y⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩$
179	177 178	breq12d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩)$
180	172	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (1), z⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩$
181	174	opeq1d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ⟨p (i), z⟩ = ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩$
182	180 181	breq12d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (⟨p (1), z⟩ Cgr ⟨p (i), z⟩ \leftrightarrow ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩)$
183	176 179 182	3anbi123d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ((⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \leftrightarrow (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
184	183	ralbidv	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (\forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \leftrightarrow \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩))$
185	171 184	3anbi12d	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to ((p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)) \leftrightarrow ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)))$
186	185	rexbidv	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (\exists z \in 𝔼 (N) (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)) \leftrightarrow \exists z \in 𝔼 (N) ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)))$
187	186	2rexbidv	$⊢ p = (k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) \to (\exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)))$
188	170 187	spcev	$⊢ \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), x⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), x⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), y⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), y⟩ \land ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (1), z⟩ Cgr ⟨(k \in (1 \dots N - 1) ⟼ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))) (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)) \to \exists p \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩))$
189	168 188	syl	$⊢ N \in ℤ_{\geq 3} \to \exists p \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) (p : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \land \forall i \in (2 \dots N - 1) (⟨p (1), x⟩ Cgr ⟨p (i), x⟩ \land ⟨p (1), y⟩ Cgr ⟨p (i), y⟩ \land ⟨p (1), z⟩ Cgr ⟨p (i), z⟩) \land \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩))$

Metamath Proof Explorer

Theorem axlowdim

Proof