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 27338

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 12638	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
2		0re 10986	. . . . 5 ⊢ 0 ∈ ℝ
3	2, 2	axlowdimlem5 27323	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
4	1, 3	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
5		1re 10984	. . . . 5 ⊢ 1 ∈ ℝ
6	5, 2	axlowdimlem5 27323	. . . 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 27323	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
9	1, 8	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
10		eqid 2739	. . . 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 27333	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁))
12		eqid 2739	. . . . . 6 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
13		eqid 2739	. . . . . 6 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
14		eqid 2739	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
15	12, 13, 14, 2, 2	axlowdimlem17 27335	. . . . 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 2739	. . . . . 6 ⊢ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
17	12, 13, 16, 5, 2	axlowdimlem17 27335	. . . . 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 2739	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))
19	12, 13, 18, 2, 5	axlowdimlem17 27335	. . . . 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 12360	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
21		peano2zm 12372	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
22	21	3ad2ant2 1133	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ)
23		2m1e1 12108	. . . . . . . . . . . . . . 15 ⊢ (2 − 1) = 1
24		2re 12056	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
25		3re 12062	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 ∈ ℝ
26		2lt3 12154	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 < 3
27	24, 25, 26	ltleii 11107	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ 3
28		zre 12332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
29		letr 11078	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
30	24, 25, 28, 29	mp3an12i 1464	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
31	27, 30	mpani 693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 ≤ 𝑁))
32	31	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
33	32	3adant1 1129	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
34	28	3ad2ant2 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
35		lesub1 11478	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1)))
36	24, 5, 35	mp3an13 1451	. . . . . . . . . . . . . . . . 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 5111	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1))
40	20, 22, 39	3jca 1127	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
41		eluz2 12597	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
42		eluz2 12597	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
43	40, 41, 42	3imtr4i 292	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ (ℤ_≥‘1))
44		eluzfz1 13272	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) → 1 ∈ (1...(𝑁 − 1)))
45	43, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 1 ∈ (1...(𝑁 − 1)))
46	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 1 ∈ (1...(𝑁 − 1)))
47		eqeq1 2743	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1))
48		oveq1 7291	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
49	48	opeq1d 4811	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ⟨(𝑘 + 1), 1⟩ = ⟨(1 + 1), 1⟩)
50	49	sneqd 4574	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → {⟨(𝑘 + 1), 1⟩} = {⟨(1 + 1), 1⟩})
51	48	sneqd 4574	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)})
52	51	difeq2d 4058	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)}))
53	52	xpeq1d 5619	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) × {0}))
54	50, 53	uneq12d 4099	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})))
55	47, 54	ifbieq2d 4486	. . . . . . . . . . 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 5355	. . . . . . . . . . . . 13 ⊢ {⟨3, -1⟩} ∈ V
57		ovex 7317	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ∈ V
58	57	difexi 5253	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {3}) ∈ V
59		snex 5355	. . . . . . . . . . . . . 14 ⊢ {0} ∈ V
60	58, 59	xpex 7612	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {3}) × {0}) ∈ V
61	56, 60	unex 7605	. . . . . . . . . . . 12 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ V
62		snex 5355	. . . . . . . . . . . . 13 ⊢ {⟨(1 + 1), 1⟩} ∈ V
63	57	difexi 5253	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(1 + 1)}) ∈ V
64	63, 59	xpex 7612	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(1 + 1)}) × {0}) ∈ V
65	62, 64	unex 7605	. . . . . . . . . . . 12 ⊢ ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈ V
66	61, 65	ifex 4510	. . . . . . . . . . 11 ⊢ if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈ V
67	55, 10, 66	fvmpt 6884	. . . . . . . . . 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 2739	. . . . . . . . . 10 ⊢ 1 = 1
70	69	iftruei 4467	. . . . . . . . 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 2795	. . . . . . . 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 4811	. . . . . . 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 12643	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
74		fzss1 13304	. . . . . . . . . . . . 13 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
75	73, 74	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
76	75	sseli 3918	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1)))
77	76	adantl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1)))
78		eqeq1 2743	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1))
79		oveq1 7291	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
80	79	opeq1d 4811	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ⟨(𝑘 + 1), 1⟩ = ⟨(𝑖 + 1), 1⟩)
81	80	sneqd 4574	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → {⟨(𝑘 + 1), 1⟩} = {⟨(𝑖 + 1), 1⟩})
82	79	sneqd 4574	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)})
83	82	difeq2d 4058	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)}))
84	83	xpeq1d 5619	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
85	81, 84	uneq12d 4099	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))
86	78, 85	ifbieq2d 4486	. . . . . . . . . . 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 5355	. . . . . . . . . . . . 13 ⊢ {⟨(𝑖 + 1), 1⟩} ∈ V
88	57	difexi 5253	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(𝑖 + 1)}) ∈ V
89	88, 59	xpex 7612	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) ∈ V
90	87, 89	unex 7605	. . . . . . . . . . . 12 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈ V
91	61, 90	ifex 4510	. . . . . . . . . . 11 ⊢ if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈ V
92	86, 10, 91	fvmpt 6884	. . . . . . . . . 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 12153	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
95	5, 24	ltnlei 11105	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
96	94, 95	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
97	96	intnanr 488	. . . . . . . . . . . . . 14 ⊢ ¬ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))
98		1z 12359	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
99		2z 12361	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
100		eluzelz 12601	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℤ)
101	100, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ ℤ)
102		elfz 13254	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
103	98, 99, 101, 102	mp3an12i 1464	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
104	97, 103	mtbiri 327	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1)))
105		eleq1 2827	. . . . . . . . . . . . . 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 407	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ¬ 𝑖 = 1)
110	109	iffalsed 4471	. . . . . . . . 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 2779	. . . . . . . 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 4811	. . . . . . 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 5088	. . . . . 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 4811	. . . . . . 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 4811	. . . . . . 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 5088	. . . . . 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 2795	. . . . . . . . 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 4811	. . . . . . . 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 481	. . . . . . 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 4811	. . . . . . 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 5088	. . . . . 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 1435	. . . . 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 1341	. . . 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 3104	. . 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 27324	. . . 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 4806	. . . . . . . 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 4806	. . . . . . . 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 5088	. . . . . . 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 1439	. . . . . 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 3113	. . . . 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 5078	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑥 Btwn ⟨𝑦, 𝑧⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩))
134		opeq2 4806	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑧, 𝑥⟩ = ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
135	134	breq2d 5087	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑦 Btwn ⟨𝑧, 𝑥⟩ ↔ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
136		opeq1 4805	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑥, 𝑦⟩ = ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)
137	136	breq2d 5087	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑧 Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩))
138	133, 135, 137	3orbi123d 1434	. . . . . 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 1438	. . . 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 4806	. . . . . . . 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 4806	. . . . . . . 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 5088	. . . . . . 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 1440	. . . . . 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 3113	. . . . 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 4805	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑦, 𝑧⟩ = ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩)
147	146	breq2d 5087	. . . . . . 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 5078	. . . . . . 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 4806	. . . . . . . 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 5087	. . . . . . 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 1434	. . . . . 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 1438	. . . 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 4806	. . . . . . . 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 4806	. . . . . . . 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 5088	. . . . . . 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 1441	. . . . . 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 3113	. . . . 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 4806	. . . . . . . 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 5087	. . . . . . 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 4805	. . . . . . . 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 5087	. . . . . . 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 5078	. . . . . . 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 1434	. . . . . 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 1438	. . . 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 3575	. . 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 1384	. 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 7317	. . . 4 ⊢ (1...(𝑁 − 1)) ∈ V
170	169	mptex 7108	. . 3 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) ∈ V
171		f1eq1 6674	. . . . . 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 6782	. . . . . . . . . 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 4811	. . . . . . . . 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 6782	. . . . . . . . . 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 4811	. . . . . . . . 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 5088	. . . . . . . 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 4811	. . . . . . . . 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 4811	. . . . . . . . 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 5088	. . . . . . . 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 4811	. . . . . . . . 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 4811	. . . . . . . . 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 5088	. . . . . . . 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 1435	. . . . . . 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 3113	. . . . . 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 1436	. . . . 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 3227	. . . 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 3230	. . 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 3546	. 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 396 ∨ w3o 1085 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2107 ∀wral 3065 ∃wrex 3066 ∖ cdif 3885 ∪ cun 3886 ⊆ wss 3888 ifcif 4460 {csn 4562 {cpr 4564 ⟨cop 4568 class class class wbr 5075 ↦ cmpt 5158 × cxp 5588 –1-1→wf1 6434 ‘cfv 6437 (class class class)co 7284 ℝcr 10879 0cc0 10880 1c1 10881 + caddc 10883 < clt 11018 ≤ cle 11019 − cmin 11214 -cneg 11215 2c2 12037 3c3 12038 ℤcz 12328 ℤ_≥cuz 12591 ...cfz 13248 𝔼cee 27265 Btwn cbtwn 27266 Cgrccgr 27267

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 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-inf2 9408 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-isom 6446 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-map 8626 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-sup 9210 df-oi 9278 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-2 12045 df-3 12046 df-n0 12243 df-z 12329 df-uz 12592 df-rp 12740 df-icc 13095 df-fz 13249 df-fzo 13392 df-seq 13731 df-exp 13792 df-hash 14054 df-cj 14819 df-re 14820 df-im 14821 df-sqrt 14955 df-abs 14956 df-clim 15206 df-sum 15407 df-ee 27268 df-btwn 27269 df-cgr 27270

This theorem is referenced by: (None)

W3C validator