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

Definition df-trkgld 25246
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
StepHypRef Expression
1 cstrkgld 25228 . 2 class DimTarskiG
2 c1 9882 . . . . . . . . . 10 class 1
3 vn . . . . . . . . . . 11 setvar 𝑛
43cv 1479 . . . . . . . . . 10 class 𝑛
5 cfzo 12403 . . . . . . . . . 10 class ..^
62, 4, 5co 6605 . . . . . . . . 9 class (1..^𝑛)
7 vp . . . . . . . . . 10 setvar 𝑝
87cv 1479 . . . . . . . . 9 class 𝑝
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1479 . . . . . . . . 9 class 𝑓
116, 8, 10wf1 5847 . . . . . . . 8 wff 𝑓:(1..^𝑛)–1-1𝑝
122, 10cfv 5850 . . . . . . . . . . . . . . . 16 class (𝑓‘1)
13 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
1413cv 1479 . . . . . . . . . . . . . . . 16 class 𝑥
15 vd . . . . . . . . . . . . . . . . 17 setvar 𝑑
1615cv 1479 . . . . . . . . . . . . . . . 16 class 𝑑
1712, 14, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑥)
18 vj . . . . . . . . . . . . . . . . . 18 setvar 𝑗
1918cv 1479 . . . . . . . . . . . . . . . . 17 class 𝑗
2019, 10cfv 5850 . . . . . . . . . . . . . . . 16 class (𝑓𝑗)
2120, 14, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑥)
2217, 21wceq 1480 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥)
23 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2423cv 1479 . . . . . . . . . . . . . . . 16 class 𝑦
2512, 24, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑦)
2620, 24, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑦)
2725, 26wceq 1480 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦)
28 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
2928cv 1479 . . . . . . . . . . . . . . . 16 class 𝑧
3012, 29, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓‘1)𝑑𝑧)
3120, 29, 16co 6605 . . . . . . . . . . . . . . 15 class ((𝑓𝑗)𝑑𝑧)
3230, 31wceq 1480 . . . . . . . . . . . . . 14 wff ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)
3322, 27, 32w3a 1036 . . . . . . . . . . . . 13 wff (((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧))
34 c2 11015 . . . . . . . . . . . . . 14 class 2
3534, 4, 5co 6605 . . . . . . . . . . . . 13 class (2..^𝑛)
3633, 18, 35wral 2912 . . . . . . . . . . . 12 wff 𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧))
37 vi . . . . . . . . . . . . . . . . 17 setvar 𝑖
3837cv 1479 . . . . . . . . . . . . . . . 16 class 𝑖
3914, 24, 38co 6605 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑦)
4029, 39wcel 1992 . . . . . . . . . . . . . 14 wff 𝑧 ∈ (𝑥𝑖𝑦)
4129, 24, 38co 6605 . . . . . . . . . . . . . . 15 class (𝑧𝑖𝑦)
4214, 41wcel 1992 . . . . . . . . . . . . . 14 wff 𝑥 ∈ (𝑧𝑖𝑦)
4314, 29, 38co 6605 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑧)
4424, 43wcel 1992 . . . . . . . . . . . . . 14 wff 𝑦 ∈ (𝑥𝑖𝑧)
4540, 42, 44w3o 1035 . . . . . . . . . . . . 13 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4645wn 3 . . . . . . . . . . . 12 wff ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
4736, 46wa 384 . . . . . . . . . . 11 wff (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4847, 28, 8wrex 2913 . . . . . . . . . 10 wff 𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4948, 23, 8wrex 2913 . . . . . . . . 9 wff 𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
5049, 13, 8wrex 2913 . . . . . . . 8 wff 𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
5111, 50wa 384 . . . . . . 7 wff (𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
5251, 9wex 1701 . . . . . 6 wff 𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
53 vg . . . . . . . 8 setvar 𝑔
5453cv 1479 . . . . . . 7 class 𝑔
55 citv 25230 . . . . . . 7 class Itv
5654, 55cfv 5850 . . . . . 6 class (Itv‘𝑔)
5752, 37, 56wsbc 3422 . . . . 5 wff [(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
58 cds 15866 . . . . . 6 class dist
5954, 58cfv 5850 . . . . 5 class (dist‘𝑔)
6057, 15, 59wsbc 3422 . . . 4 wff [(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
61 cbs 15776 . . . . 5 class Base
6254, 61cfv 5850 . . . 4 class (Base‘𝑔)
6360, 7, 62wsbc 3422 . . 3 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
6463, 53, 3copab 4677 . 2 class {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
651, 64wceq 1480 1 wff DimTarskiG≥ = {⟨𝑔, 𝑛⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑓(𝑓:(1..^𝑛)–1-1𝑝 ∧ ∃𝑥𝑝𝑦𝑝𝑧𝑝 (∀𝑗 ∈ (2..^𝑛)(((𝑓‘1)𝑑𝑥) = ((𝑓𝑗)𝑑𝑥) ∧ ((𝑓‘1)𝑑𝑦) = ((𝑓𝑗)𝑑𝑦) ∧ ((𝑓‘1)𝑑𝑧) = ((𝑓𝑗)𝑑𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgld  25253
  Copyright terms: Public domain W3C validator