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

Definition df-trkgld 24579
 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 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 Itv ..^ ..^
Distinct variable group:   ,,,,,,,,,

Detailed syntax breakdown of Definition df-trkgld
StepHypRef Expression
1 cstrkgld 24561 . 2 DimTarskiG
2 c1 9558 . . . . . . . . . 10
3 vn . . . . . . . . . . 11
43cv 1451 . . . . . . . . . 10
5 cfzo 11942 . . . . . . . . . 10 ..^
62, 4, 5co 6308 . . . . . . . . 9 ..^
7 vp . . . . . . . . . 10
87cv 1451 . . . . . . . . 9
9 vf . . . . . . . . . 10
109cv 1451 . . . . . . . . 9
116, 8, 10wf1 5586 . . . . . . . 8 ..^
122, 10cfv 5589 . . . . . . . . . . . . . . . 16
13 vx . . . . . . . . . . . . . . . . 17
1413cv 1451 . . . . . . . . . . . . . . . 16
15 vd . . . . . . . . . . . . . . . . 17
1615cv 1451 . . . . . . . . . . . . . . . 16
1712, 14, 16co 6308 . . . . . . . . . . . . . . 15
18 vj . . . . . . . . . . . . . . . . . 18
1918cv 1451 . . . . . . . . . . . . . . . . 17
2019, 10cfv 5589 . . . . . . . . . . . . . . . 16
2120, 14, 16co 6308 . . . . . . . . . . . . . . 15
2217, 21wceq 1452 . . . . . . . . . . . . . 14
23 vy . . . . . . . . . . . . . . . . 17
2423cv 1451 . . . . . . . . . . . . . . . 16
2512, 24, 16co 6308 . . . . . . . . . . . . . . 15
2620, 24, 16co 6308 . . . . . . . . . . . . . . 15
2725, 26wceq 1452 . . . . . . . . . . . . . 14
28 vz . . . . . . . . . . . . . . . . 17
2928cv 1451 . . . . . . . . . . . . . . . 16
3012, 29, 16co 6308 . . . . . . . . . . . . . . 15
3120, 29, 16co 6308 . . . . . . . . . . . . . . 15
3230, 31wceq 1452 . . . . . . . . . . . . . 14
3322, 27, 32w3a 1007 . . . . . . . . . . . . 13
34 c2 10681 . . . . . . . . . . . . . 14
3534, 4, 5co 6308 . . . . . . . . . . . . 13 ..^
3633, 18, 35wral 2756 . . . . . . . . . . . 12 ..^
37 vi . . . . . . . . . . . . . . . . 17
3837cv 1451 . . . . . . . . . . . . . . . 16
3914, 24, 38co 6308 . . . . . . . . . . . . . . 15
4029, 39wcel 1904 . . . . . . . . . . . . . 14
4129, 24, 38co 6308 . . . . . . . . . . . . . . 15
4214, 41wcel 1904 . . . . . . . . . . . . . 14
4314, 29, 38co 6308 . . . . . . . . . . . . . . 15
4424, 43wcel 1904 . . . . . . . . . . . . . 14
4540, 42, 44w3o 1006 . . . . . . . . . . . . 13
4645wn 3 . . . . . . . . . . . 12
4736, 46wa 376 . . . . . . . . . . 11 ..^
4847, 28, 8wrex 2757 . . . . . . . . . 10 ..^
4948, 23, 8wrex 2757 . . . . . . . . 9 ..^
5049, 13, 8wrex 2757 . . . . . . . 8 ..^
5111, 50wa 376 . . . . . . 7 ..^ ..^
5251, 9wex 1671 . . . . . 6 ..^ ..^
53 vg . . . . . . . 8
5453cv 1451 . . . . . . 7
55 citv 24563 . . . . . . 7 Itv
5654, 55cfv 5589 . . . . . 6 Itv
5752, 37, 56wsbc 3255 . . . . 5 Itv ..^ ..^
58 cds 15277 . . . . . 6
5954, 58cfv 5589 . . . . 5
6057, 15, 59wsbc 3255 . . . 4 Itv ..^ ..^
61 cbs 15199 . . . . 5
6254, 61cfv 5589 . . . 4
6360, 7, 62wsbc 3255 . . 3 Itv ..^ ..^
6463, 53, 3copab 4453 . 2 Itv ..^ ..^
651, 64wceq 1452 1 DimTarskiG Itv ..^ ..^
 Colors of variables: wff setvar class This definition is referenced by:  istrkgld  24586
 Copyright terms: Public domain W3C validator