Metamath Proof Explorer

Definition df-trkgld

Description: Define the class of geometries fulfilling the lower dimension axiom for dimension n . For such geometries, there are three non-colinear points that are equidistant from n - 1 distinct points. Derived from remarks inTarski'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)

Ref Expression
Assertion df-trkgld ⊢ Dim 𝒢 ≥ = g n | [˙Base g / p]˙ [˙ dist ⁡ g / d]˙ [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgld class Dim 𝒢 ≥
1 vg setvar g
2 vn setvar n
3 cbs class Base
4 1 cv setvar g
5 4 3 cfv class Base g
6 vp setvar p
7 cds class dist
8 4 7 cfv class dist ⁡ g
9 vd setvar d
10 citv class Itv
11 4 10 cfv class Itv ⁡ g
12 vi setvar i
13 vf setvar f
14 13 cv setvar f
15 c1 class 1
16 cfzo class ..^
17 2 cv setvar n
18 15 17 16 co class 1 ..^ n
19 6 cv setvar p
20 18 19 14 wf1 wff f : 1 ..^ n ⟶ 1-1 p
21 vx setvar x
22 vy setvar y
23 vz setvar z
24 vj setvar j
25 c2 class 2
26 25 17 16 co class 2 ..^ n
27 15 14 cfv class f ⁡ 1
28 9 cv setvar d
29 21 cv setvar x
30 27 29 28 co class f ⁡ 1 d x
31 24 cv setvar j
32 31 14 cfv class f ⁡ j
33 32 29 28 co class f ⁡ j d x
34 30 33 wceq wff f ⁡ 1 d x = f ⁡ j d x
35 22 cv setvar y
36 27 35 28 co class f ⁡ 1 d y
37 32 35 28 co class f ⁡ j d y
38 36 37 wceq wff f ⁡ 1 d y = f ⁡ j d y
39 23 cv setvar z
40 27 39 28 co class f ⁡ 1 d z
41 32 39 28 co class f ⁡ j d z
42 40 41 wceq wff f ⁡ 1 d z = f ⁡ j d z
43 34 38 42 w3a wff f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z
44 43 24 26 wral wff ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z
45 12 cv setvar i
46 29 35 45 co class x i y
47 39 46 wcel wff z ∈ x i y
48 39 35 45 co class z i y
49 29 48 wcel wff x ∈ z i y
50 29 39 45 co class x i z
51 35 50 wcel wff y ∈ x i z
52 47 49 51 w3o wff z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
53 52 wn wff ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
54 44 53 wa wff ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
55 54 23 19 wrex wff ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
56 55 22 19 wrex wff ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
57 56 21 19 wrex wff ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
58 20 57 wa wff f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
59 58 13 wex wff ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
60 59 12 11 wsbc wff [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
61 60 9 8 wsbc wff [˙ dist ⁡ g / d]˙ [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
62 61 6 5 wsbc wff [˙Base g / p]˙ [˙ dist ⁡ g / d]˙ [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
63 62 1 2 copab class g n | [˙Base g / p]˙ [˙ dist ⁡ g / d]˙ [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
64 0 63 wceq wff Dim 𝒢 ≥ = g n | [˙Base g / p]˙ [˙ dist ⁡ g / d]˙ [˙ Itv ⁡ g / i]˙ ∃ f f : 1 ..^ n ⟶ 1-1 p ∧ ∃ x ∈ p ∃ y ∈ p ∃ z ∈ p ∀ j ∈ 2 ..^ n f ⁡ 1 d x = f ⁡ j d x ∧ f ⁡ 1 d y = f ⁡ j d y ∧ f ⁡ 1 d z = f ⁡ j d z ∧ ¬ z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z