axlowdim - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axlowdim		Structured version Visualization version GIF version

Theorem axlowdim 28219

Description: The general lower dimension axiom. Take a dimension 𝑁 greater than or equal to three. Then, there are three non-colinear points in 𝑁 dimensional space that are equidistant from 𝑁 − 1 distinct points. Derived from remarks in Tarski'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.)

**Assertion**
Ref	Expression
axlowdim	⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)))

Distinct variable group: 𝑖,𝑁,𝑝,𝑥,𝑦,𝑧

Proof of Theorem axlowdim Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		uzuzle23 12873	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
2		0re 11216	. . . . 5 ⊢ 0 ∈ ℝ
3	2, 2	axlowdimlem5 28204	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
4	1, 3	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
5		1re 11214	. . . . 5 ⊢ 1 ∈ ℝ
6	5, 2	axlowdimlem5 28204	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
7	1, 6	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
8	2, 5	axlowdimlem5 28204	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
9	1, 8	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
10		eqid 2733	. . . 4 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))
11	10	axlowdimlem15 28214	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁))
12		eqid 2733	. . . . . 6 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
13		eqid 2733	. . . . . 6 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
14		eqid 2733	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
15	12, 13, 14, 2, 2	axlowdimlem17 28216	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
16		eqid 2733	. . . . . 6 ⊢ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
17	12, 13, 16, 5, 2	axlowdimlem17 28216	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
18		eqid 2733	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))
19	12, 13, 18, 2, 5	axlowdimlem17 28216	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
20		1zzd 12593	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
21		peano2zm 12605	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
22	21	3ad2ant2 1135	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ)
23		2m1e1 12338	. . . . . . . . . . . . . . 15 ⊢ (2 − 1) = 1
24		2re 12286	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
25		3re 12292	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 ∈ ℝ
26		2lt3 12384	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 < 3
27	24, 25, 26	ltleii 11337	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ 3
28		zre 12562	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
29		letr 11308	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
30	24, 25, 28, 29	mp3an12i 1466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
31	27, 30	mpani 695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 ≤ 𝑁))
32	31	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
33	32	3adant1 1131	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
34	28	3ad2ant2 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
35		lesub1 11708	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1)))
36	24, 5, 35	mp3an13 1453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℝ → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1)))
37	34, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1)))
38	33, 37	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (2 − 1) ≤ (𝑁 − 1))
39	23, 38	eqbrtrrid 5185	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1))
40	20, 22, 39	3jca 1129	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
41		eluz2 12828	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
42		eluz2 12828	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
43	40, 41, 42	3imtr4i 292	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ (ℤ_≥‘1))
44		eluzfz1 13508	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 − 1)))
45	43, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (1...(𝑁 − 1)))
46	45	adantr 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 1 ∈ (1...(𝑁 − 1)))
47		eqeq1 2737	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1))
48		oveq1 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
49	48	opeq1d 4880	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ⟨(𝑘 + 1), 1⟩ = ⟨(1 + 1), 1⟩)
50	49	sneqd 4641	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → {⟨(𝑘 + 1), 1⟩} = {⟨(1 + 1), 1⟩})
51	48	sneqd 4641	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)})
52	51	difeq2d 4123	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)}))
53	52	xpeq1d 5706	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) × {0}))
54	50, 53	uneq12d 4165	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})))
55	47, 54	ifbieq2d 4555	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))))
56		snex 5432	. . . . . . . . . . . . 13 ⊢ {⟨3, -1⟩} ∈ V
57		ovex 7442	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ∈ V
58	57	difexi 5329	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {3}) ∈ V
59		snex 5432	. . . . . . . . . . . . . 14 ⊢ {0} ∈ V
60	58, 59	xpex 7740	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {3}) × {0}) ∈ V
61	56, 60	unex 7733	. . . . . . . . . . . 12 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ V
62		snex 5432	. . . . . . . . . . . . 13 ⊢ {⟨(1 + 1), 1⟩} ∈ V
63	57	difexi 5329	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(1 + 1)}) ∈ V
64	63, 59	xpex 7740	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(1 + 1)}) × {0}) ∈ V
65	62, 64	unex 7733	. . . . . . . . . . . 12 ⊢ ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈ V
66	61, 65	ifex 4579	. . . . . . . . . . 11 ⊢ if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈ V
67	55, 10, 66	fvmpt 6999	. . . . . . . . . 10 ⊢ (1 ∈ (1...(𝑁 − 1)) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))))
68	46, 67	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))))
69		eqid 2733	. . . . . . . . . 10 ⊢ 1 = 1
70	69	iftruei 4536	. . . . . . . . 9 ⊢ if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
71	68, 70	eqtrdi 2789	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
72	71	opeq1d 4880	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
73		2eluzge1 12878	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
74		fzss1 13540	. . . . . . . . . . . . 13 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
75	73, 74	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
76	75	sseli 3979	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1)))
77	76	adantl 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1)))
78		eqeq1 2737	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1))
79		oveq1 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
80	79	opeq1d 4880	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ⟨(𝑘 + 1), 1⟩ = ⟨(𝑖 + 1), 1⟩)
81	80	sneqd 4641	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → {⟨(𝑘 + 1), 1⟩} = {⟨(𝑖 + 1), 1⟩})
82	79	sneqd 4641	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)})
83	82	difeq2d 4123	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)}))
84	83	xpeq1d 5706	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
85	81, 84	uneq12d 4165	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))
86	78, 85	ifbieq2d 4555	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))))
87		snex 5432	. . . . . . . . . . . . 13 ⊢ {⟨(𝑖 + 1), 1⟩} ∈ V
88	57	difexi 5329	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(𝑖 + 1)}) ∈ V
89	88, 59	xpex 7740	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) ∈ V
90	87, 89	unex 7733	. . . . . . . . . . . 12 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈ V
91	61, 90	ifex 4579	. . . . . . . . . . 11 ⊢ if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈ V
92	86, 10, 91	fvmpt 6999	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑁 − 1)) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖) = if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))))
93	77, 92	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖) = if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))))
94		1lt2 12383	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
95	5, 24	ltnlei 11335	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
96	94, 95	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
97	96	intnanr 489	. . . . . . . . . . . . . 14 ⊢ ¬ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))
98		1z 12592	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
99		2z 12594	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
100		eluzelz 12832	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℤ)
101	100, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ ℤ)
102		elfz 13490	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
103	98, 99, 101, 102	mp3an12i 1466	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
104	97, 103	mtbiri 327	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1)))
105		eleq1 2822	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (𝑖 ∈ (2...(𝑁 − 1)) ↔ 1 ∈ (2...(𝑁 − 1))))
106	105	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (¬ 𝑖 ∈ (2...(𝑁 − 1)) ↔ ¬ 1 ∈ (2...(𝑁 − 1))))
107	104, 106	syl5ibrcom 246	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑖 = 1 → ¬ 𝑖 ∈ (2...(𝑁 − 1))))
108	107	con2d 134	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑖 ∈ (2...(𝑁 − 1)) → ¬ 𝑖 = 1))
109	108	imp 408	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ¬ 𝑖 = 1)
110	109	iffalsed 4540	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))
111	93, 110	eqtrd 2773	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))
112	111	opeq1d 4880	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
113	72, 112	breq12d 5162	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
114	71	opeq1d 4880	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
115	111	opeq1d 4880	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
116	114, 115	breq12d 5162	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
117	45, 67	syl 17	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))))
118	117, 70	eqtrdi 2789	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
119	118	opeq1d 4880	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
120	119	adantr 482	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
121	111	opeq1d 4880	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
122	120, 121	breq12d 5162	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩))
123	113, 116, 122	3anbi123d 1437	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩) ↔ (⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)))
124	15, 17, 19, 123	mpbir3and 1343	. . . 4 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩))
125	124	ralrimiva 3147	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩))
126	14, 16, 18	axlowdimlem6 28205	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
127	1, 126	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
128		opeq2 4875	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
129		opeq2 4875	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
130	128, 129	breq12d 5162	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
131	130	3anbi1d 1441	. . . . . 6 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ((⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
132	131	ralbidv 3178	. . . . 5 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
133		breq1 5152	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑥 Btwn ⟨𝑦, 𝑧⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩))
134		opeq2 4875	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑧, 𝑥⟩ = ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
135	134	breq2d 5161	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑦 Btwn ⟨𝑧, 𝑥⟩ ↔ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
136		opeq1 4874	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑥, 𝑦⟩ = ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)
137	136	breq2d 5161	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑧 Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩))
138	133, 135, 137	3orbi123d 1436	. . . . . 6 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ((𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩) ↔ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)))
139	138	notbid 318	. . . . 5 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩) ↔ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)))
140	132, 139	3anbi23d 1440	. . . 4 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩))))
141		opeq2 4875	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
142		opeq2 4875	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
143	141, 142	breq12d 5162	. . . . . . 7 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
144	143	3anbi2d 1442	. . . . . 6 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ((⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
145	144	ralbidv 3178	. . . . 5 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
146		opeq1 4874	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑦, 𝑧⟩ = ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩)
147	146	breq2d 5161	. . . . . . 7 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩))
148		breq1 5152	. . . . . . 7 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
149		opeq2 4875	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩ = ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
150	149	breq2d 5161	. . . . . . 7 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩ ↔ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
151	147, 148, 150	3orbi123d 1436	. . . . . 6 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ((({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩) ↔ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)))
152	151	notbid 318	. . . . 5 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩) ↔ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)))
153	145, 152	3anbi23d 1440	. . . 4 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))))
154		opeq2 4875	. . . . . . . 8 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
155		opeq2 4875	. . . . . . . 8 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
156	154, 155	breq12d 5162	. . . . . . 7 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩))
157	156	3anbi3d 1443	. . . . . 6 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ((⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)))
158	157	ralbidv 3178	. . . . 5 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)))
159		opeq2 4875	. . . . . . . 8 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ = ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
160	159	breq2d 5161	. . . . . . 7 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩))
161		opeq1 4874	. . . . . . . 8 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ = ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
162	161	breq2d 5161	. . . . . . 7 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
163		breq1 5152	. . . . . . 7 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ↔ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
164	160, 162, 163	3orbi123d 1436	. . . . . 6 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → ((({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩) ↔ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)))
165	164	notbid 318	. . . . 5 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩) ↔ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)))
166	158, 165	3anbi23d 1440	. . . 4 ⊢ (𝑧 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) → (((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))))
167	140, 153, 166	rspc3ev 3629	. . 3 ⊢ (((({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁)) ∧ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩) ∧ ¬ (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩ ∨ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)))
168	4, 7, 9, 11, 125, 127, 167	syl33anc 1386	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)))
169		ovex 7442	. . . 4 ⊢ (1...(𝑁 − 1)) ∈ V
170	169	mptex 7225	. . 3 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) ∈ V
171		f1eq1 6783	. . . . . 6 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁)))
172		fveq1 6891	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (𝑝‘1) = ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1))
173	172	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘1), 𝑥⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩)
174		fveq1 6891	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (𝑝‘𝑖) = ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖))
175	174	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘𝑖), 𝑥⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩)
176	173, 175	breq12d 5162	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩))
177	172	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘1), 𝑦⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩)
178	174	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘𝑖), 𝑦⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩)
179	177, 178	breq12d 5162	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩))
180	172	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘1), 𝑧⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩)
181	174	opeq1d 4880	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ⟨(𝑝‘𝑖), 𝑧⟩ = ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)
182	180, 181	breq12d 5162	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩ ↔ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩))
183	176, 179, 182	3anbi123d 1437	. . . . . . 7 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ((⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ↔ (⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
184	183	ralbidv 3178	. . . . . 6 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩)))
185	171, 184	3anbi12d 1438	. . . . 5 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → ((𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩))))
186	185	rexbidv 3179	. . . 4 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)) ↔ ∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩))))
187	186	2rexbidv 3220	. . 3 ⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩))))
188	170, 187	spcev 3597	. 2 ⊢ (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑥⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑥⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑦⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑦⟩ ∧ ⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), 𝑧⟩Cgr⟨((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)))
189	168, 188	syl 17	1 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(⟨(𝑝‘1), 𝑥⟩Cgr⟨(𝑝‘𝑖), 𝑥⟩ ∧ ⟨(𝑝‘1), 𝑦⟩Cgr⟨(𝑝‘𝑖), 𝑦⟩ ∧ ⟨(𝑝‘1), 𝑧⟩Cgr⟨(𝑝‘𝑖), 𝑧⟩) ∧ ¬ (𝑥 Btwn ⟨𝑦, 𝑧⟩ ∨ 𝑦 Btwn ⟨𝑧, 𝑥⟩ ∨ 𝑧 Btwn ⟨𝑥, 𝑦⟩)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ w3o 1087 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 ∖ cdif 3946 ∪ cun 3947 ⊆ wss 3949 ifcif 4529 {csn 4629 {cpr 4631 ⟨cop 4635 class class class wbr 5149 ↦ cmpt 5232 × cxp 5675 –1-1→wf1 6541 ‘cfv 6544 (class class class)co 7409 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 < clt 11248 ≤ cle 11249 − cmin 11444 -cneg 11445 2c2 12267 3c3 12268 ℤcz 12558 ℤ_≥cuz 12822 ...cfz 13484 𝔼cee 28146 Btwn cbtwn 28147 Cgrccgr 28148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-oi 9505 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-n0 12473 df-z 12559 df-uz 12823 df-rp 12975 df-icc 13331 df-fz 13485 df-fzo 13628 df-seq 13967 df-exp 14028 df-hash 14291 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-clim 15432 df-sum 15633 df-ee 28149 df-btwn 28150 df-cgr 28151

This theorem is referenced by: (None)

W3C validator