Definition df-trkgld 27970

Description: Define the class of geometries fulfilling the lower dimension axiom for dimension 𝑛. For such geometries, there are three non-colinear points 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.) (Revised by Thierry Arnoux, 23-Nov-2019.)

Assertion

Ref	Expression
df-trkgld	⊢ DimTarskiG≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}

Distinct variable group:   𝑓,𝑑,𝑔,𝑛,𝑝,𝑖,𝑗,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgld

Step	Hyp	Ref	Expression
1		cstrkgld 27949	. 2 class DimTarskiG≥
2		c1 11113	. . . . . . . . . 10 class 1
3		vn	. . . . . . . . . . 11 setvar 𝑛
4	3	cv 1538	. . . . . . . . . 10 class 𝑛
5		cfzo 13631	. . . . . . . . . 10 class ..^
6	2, 4, 5	co 7411	. . . . . . . . 9 class (1..^𝑛)
7		vp	. . . . . . . . . 10 setvar 𝑝
8	7	cv 1538	. . . . . . . . 9 class 𝑝
9		vf	. . . . . . . . . 10 setvar 𝑓
10	9	cv 1538	. . . . . . . . 9 class 𝑓
11	6, 8, 10	wf1 6539	. . . . . . . 8 wff 𝑓:(1..^𝑛)–1-1→𝑝
12	2, 10	cfv 6542	. . . . . . . . . . . . . . . 16 class (𝑓‘1)
13		vx	. . . . . . . . . . . . . . . . 17 setvar 𝑥
14	13	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑥
15		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
16	15	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑑
17	12, 14, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑥)
18		vj	. . . . . . . . . . . . . . . . . 18 setvar 𝑗
19	18	cv 1538	. . . . . . . . . . . . . . . . 17 class 𝑗
20	19, 10	cfv 6542	. . . . . . . . . . . . . . . 16 class (𝑓‘𝑗)
21	20, 14, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘𝑗)𝑑𝑥)
22	17, 21	wceq 1539	. . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥)
23		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
24	23	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑦
25	12, 24, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑦)
26	20, 24, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘𝑗)𝑑𝑦)
27	25, 26	wceq 1539	. . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦)
28		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
29	28	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑧
30	12, 29, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑧)
31	20, 29, 16	co 7411	. . . . . . . . . . . . . . 15 class ((𝑓‘𝑗)𝑑𝑧)
32	30, 31	wceq 1539	. . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)
33	22, 27, 32	w3a 1085	. . . . . . . . . . . . 13 wff (((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧))
34		c2 12271	. . . . . . . . . . . . . 14 class 2
35	34, 4, 5	co 7411	. . . . . . . . . . . . 13 class (2..^𝑛)
36	33, 18, 35	wral 3059	. . . . . . . . . . . 12 wff ∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧))
37		vi	. . . . . . . . . . . . . . . . 17 setvar 𝑖
38	37	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑖
39	14, 24, 38	co 7411	. . . . . . . . . . . . . . 15 class (𝑥𝑖𝑦)
40	29, 39	wcel 2104	. . . . . . . . . . . . . 14 wff 𝑧 ∈ (𝑥𝑖𝑦)
41	29, 24, 38	co 7411	. . . . . . . . . . . . . . 15 class (𝑧𝑖𝑦)
42	14, 41	wcel 2104	. . . . . . . . . . . . . 14 wff 𝑥 ∈ (𝑧𝑖𝑦)
43	14, 29, 38	co 7411	. . . . . . . . . . . . . . 15 class (𝑥𝑖𝑧)
44	24, 43	wcel 2104	. . . . . . . . . . . . . 14 wff 𝑦 ∈ (𝑥𝑖𝑧)
45	40, 42, 44	w3o 1084	. . . . . . . . . . . . 13 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
46	45	wn 3	. . . . . . . . . . . 12 wff ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
47	36, 46	wa 394	. . . . . . . . . . 11 wff (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
48	47, 28, 8	wrex 3068	. . . . . . . . . 10 wff ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
49	48, 23, 8	wrex 3068	. . . . . . . . 9 wff ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
50	49, 13, 8	wrex 3068	. . . . . . . 8 wff ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
51	11, 50	wa 394	. . . . . . 7 wff (𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
52	51, 9	wex 1779	. . . . . 6 wff ∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
53		vg	. . . . . . . 8 setvar 𝑔
54	53	cv 1538	. . . . . . 7 class 𝑔
55		citv 27951	. . . . . . 7 class Itv
56	54, 55	cfv 6542	. . . . . 6 class (Itv‘𝑔)
57	52, 37, 56	wsbc 3776	. . . . 5 wff [(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
58		cds 17210	. . . . . 6 class dist
59	54, 58	cfv 6542	. . . . 5 class (dist‘𝑔)
60	57, 15, 59	wsbc 3776	. . . 4 wff [(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
61		cbs 17148	. . . . 5 class Base
62	54, 61	cfv 6542	. . . 4 class (Base‘𝑔)
63	60, 7, 62	wsbc 3776	. . 3 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
64	63, 53, 3	copab 5209	. 2 class {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
65	1, 64	wceq 1539	1 wff DimTarskiG≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑓(𝑓:(1..^𝑛)–1-1→𝑝 ∧ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓‘𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓‘𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓‘𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}

This definition is referenced by:  istrkgld  27977