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 27910

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 12814	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
2		0re 11157	. . . . 5 ⊢ 0 ∈ ℝ
3	2, 2	axlowdimlem5 27895	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
4	1, 3	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
5		1re 11155	. . . . 5 ⊢ 1 ∈ ℝ
6	5, 2	axlowdimlem5 27895	. . . 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 27895	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘2) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
9	1, 8	syl 17	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
10		eqid 2736	. . . 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 27905	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))):(1...(𝑁 − 1))–1-1→(𝔼‘𝑁))
12		eqid 2736	. . . . . 6 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
13		eqid 2736	. . . . . 6 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
14		eqid 2736	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
15	12, 13, 14, 2, 2	axlowdimlem17 27907	. . . . 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 2736	. . . . . 6 ⊢ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
17	12, 13, 16, 5, 2	axlowdimlem17 27907	. . . . 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 2736	. . . . . 6 ⊢ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))
19	12, 13, 18, 2, 5	axlowdimlem17 27907	. . . . 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 12534	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
21		peano2zm 12546	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
22	21	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ)
23		2m1e1 12279	. . . . . . . . . . . . . . 15 ⊢ (2 − 1) = 1
24		2re 12227	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
25		3re 12233	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 ∈ ℝ
26		2lt3 12325	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 < 3
27	24, 25, 26	ltleii 11278	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ 3
28		zre 12503	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
29		letr 11249	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
30	24, 25, 28, 29	mp3an12i 1465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → ((2 ≤ 3 ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁))
31	27, 30	mpani 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℤ → (3 ≤ 𝑁 → 2 ≤ 𝑁))
32	31	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
33	32	3adant1 1130	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁)
34	28	3ad2ant2 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
35		lesub1 11649	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1)))
36	24, 5, 35	mp3an13 1452	. . . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1))
40	20, 22, 39	3jca 1128	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
41		eluz2 12769	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁))
42		eluz2 12769	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 1 ≤ (𝑁 − 1)))
43	40, 41, 42	3imtr4i 291	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ (ℤ_≥‘1))
44		eluzfz1 13448	. . . . . . . . . . . 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 2740	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1))
48		oveq1 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
49	48	opeq1d 4836	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ⟨(𝑘 + 1), 1⟩ = ⟨(1 + 1), 1⟩)
50	49	sneqd 4598	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → {⟨(𝑘 + 1), 1⟩} = {⟨(1 + 1), 1⟩})
51	48	sneqd 4598	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)})
52	51	difeq2d 4082	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)}))
53	52	xpeq1d 5662	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) × {0}))
54	50, 53	uneq12d 4124	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})))
55	47, 54	ifbieq2d 4512	. . . . . . . . . . 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 5388	. . . . . . . . . . . . 13 ⊢ {⟨3, -1⟩} ∈ V
57		ovex 7390	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ∈ V
58	57	difexi 5285	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {3}) ∈ V
59		snex 5388	. . . . . . . . . . . . . 14 ⊢ {0} ∈ V
60	58, 59	xpex 7687	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {3}) × {0}) ∈ V
61	56, 60	unex 7680	. . . . . . . . . . . 12 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ V
62		snex 5388	. . . . . . . . . . . . 13 ⊢ {⟨(1 + 1), 1⟩} ∈ V
63	57	difexi 5285	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(1 + 1)}) ∈ V
64	63, 59	xpex 7687	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(1 + 1)}) × {0}) ∈ V
65	62, 64	unex 7680	. . . . . . . . . . . 12 ⊢ ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈ V
66	61, 65	ifex 4536	. . . . . . . . . . 11 ⊢ if(1 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈ V
67	55, 10, 66	fvmpt 6948	. . . . . . . . . 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 2736	. . . . . . . . . 10 ⊢ 1 = 1
70	69	iftruei 4493	. . . . . . . . 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 2792	. . . . . . . 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 4836	. . . . . . 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 12819	. . . . . . . . . . . . 13 ⊢ 2 ∈ (ℤ_≥‘1)
74		fzss1 13480	. . . . . . . . . . . . 13 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
75	73, 74	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))
76	75	sseli 3940	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1)))
77	76	adantl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1)))
78		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1))
79		oveq1 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
80	79	opeq1d 4836	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ⟨(𝑘 + 1), 1⟩ = ⟨(𝑖 + 1), 1⟩)
81	80	sneqd 4598	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → {⟨(𝑘 + 1), 1⟩} = {⟨(𝑖 + 1), 1⟩})
82	79	sneqd 4598	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)})
83	82	difeq2d 4082	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)}))
84	83	xpeq1d 5662	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
85	81, 84	uneq12d 4124	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))
86	78, 85	ifbieq2d 4512	. . . . . . . . . . 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 5388	. . . . . . . . . . . . 13 ⊢ {⟨(𝑖 + 1), 1⟩} ∈ V
88	57	difexi 5285	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ∖ {(𝑖 + 1)}) ∈ V
89	88, 59	xpex 7687	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) ∈ V
90	87, 89	unex 7680	. . . . . . . . . . . 12 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈ V
91	61, 90	ifex 4536	. . . . . . . . . . 11 ⊢ if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈ V
92	86, 10, 91	fvmpt 6948	. . . . . . . . . 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 12324	. . . . . . . . . . . . . . . 16 ⊢ 1 < 2
95	5, 24	ltnlei 11276	. . . . . . . . . . . . . . . 16 ⊢ (1 < 2 ↔ ¬ 2 ≤ 1)
96	94, 95	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ≤ 1
97	96	intnanr 488	. . . . . . . . . . . . . 14 ⊢ ¬ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))
98		1z 12533	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
99		2z 12535	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
100		eluzelz 12773	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℤ)
101	100, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 1) ∈ ℤ)
102		elfz 13430	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
103	98, 99, 101, 102	mp3an12i 1465	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1))))
104	97, 103	mtbiri 326	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1)))
105		eleq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (𝑖 ∈ (2...(𝑁 − 1)) ↔ 1 ∈ (2...(𝑁 − 1))))
106	105	notbid 317	. . . . . . . . . . . . 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 4497	. . . . . . . . 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 2776	. . . . . . . 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 4836	. . . . . . 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 5118	. . . . . 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 4836	. . . . . . 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 4836	. . . . . . 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 5118	. . . . . 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 2792	. . . . . . . . 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 4836	. . . . . . . 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 4836	. . . . . . 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 5118	. . . . . 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 1436	. . . . 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 1342	. . . 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 3143	. . 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 27896	. . . 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 4831	. . . . . . . 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 4831	. . . . . . . 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 5118	. . . . . . 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 1440	. . . . . 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 3174	. . . . 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 5108	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑥 Btwn ⟨𝑦, 𝑧⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩))
134		opeq2 4831	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑧, 𝑥⟩ = ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
135	134	breq2d 5117	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑦 Btwn ⟨𝑧, 𝑥⟩ ↔ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩))
136		opeq1 4830	. . . . . . . 8 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑥, 𝑦⟩ = ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩)
137	136	breq2d 5117	. . . . . . 7 ⊢ (𝑥 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → (𝑧 Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑦⟩))
138	133, 135, 137	3orbi123d 1435	. . . . . 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 317	. . . . 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 1439	. . . 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 4831	. . . . . . . 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 4831	. . . . . . . 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 5118	. . . . . . 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 1441	. . . . . 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 3174	. . . . 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 4830	. . . . . . . 8 ⊢ (𝑦 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) → ⟨𝑦, 𝑧⟩ = ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), 𝑧⟩)
147	146	breq2d 5117	. . . . . . 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 5108	. . . . . . 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 4831	. . . . . . . 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 5117	. . . . . . 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 1435	. . . . . 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 317	. . . . 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 1439	. . . 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 4831	. . . . . . . 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 4831	. . . . . . . 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 5118	. . . . . . 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 1442	. . . . . 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 3174	. . . . 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 4831	. . . . . . . 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 5117	. . . . . . 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 4830	. . . . . . . 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 5117	. . . . . . 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 5108	. . . . . . 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 1435	. . . . . 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 317	. . . . 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 1439	. . . 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 3594	. . 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 1385	. 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 7390	. . . 4 ⊢ (1...(𝑁 − 1)) ∈ V
170	169	mptex 7173	. . 3 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) ∈ V
171		f1eq1 6733	. . . . . 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 6841	. . . . . . . . . 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 4836	. . . . . . . . 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 6841	. . . . . . . . . 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 4836	. . . . . . . . 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 5118	. . . . . . . 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 4836	. . . . . . . . 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 4836	. . . . . . . . 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 5118	. . . . . . . 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 4836	. . . . . . . . 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 4836	. . . . . . . . 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 5118	. . . . . . . 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 1436	. . . . . . 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 3174	. . . . . 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 1437	. . . . 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 3175	. . . 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 3213	. . 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 3565	. 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 1086 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 ∖ cdif 3907 ∪ cun 3908 ⊆ wss 3910 ifcif 4486 {csn 4586 {cpr 4588 ⟨cop 4592 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 –1-1→wf1 6493 ‘cfv 6496 (class class class)co 7357 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 2c2 12208 3c3 12209 ℤcz 12499 ℤ_≥cuz 12763 ...cfz 13424 𝔼cee 27837 Btwn cbtwn 27838 Cgrccgr 27839

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9378 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-icc 13271 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-sum 15571 df-ee 27840 df-btwn 27841 df-cgr 27842

This theorem is referenced by: (None)

W3C validator