Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trkg2d Structured version   Visualization version   GIF version

Definition df-trkg2d 29996
Description: Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.) (New usage is discouraged.)
Assertion
Ref Expression
df-trkg2d TarskiG2D = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Distinct variable group:   𝑓,𝑑,𝑖,𝑝,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkg2d
StepHypRef Expression
1 cstrkg2d 29995 . 2 class TarskiG2D
2 vz . . . . . . . . . . . . . 14 setvar 𝑧
32cv 1474 . . . . . . . . . . . . 13 class 𝑧
4 vx . . . . . . . . . . . . . . 15 setvar 𝑥
54cv 1474 . . . . . . . . . . . . . 14 class 𝑥
6 vy . . . . . . . . . . . . . . 15 setvar 𝑦
76cv 1474 . . . . . . . . . . . . . 14 class 𝑦
8 vi . . . . . . . . . . . . . . 15 setvar 𝑖
98cv 1474 . . . . . . . . . . . . . 14 class 𝑖
105, 7, 9co 6549 . . . . . . . . . . . . 13 class (𝑥𝑖𝑦)
113, 10wcel 1977 . . . . . . . . . . . 12 wff 𝑧 ∈ (𝑥𝑖𝑦)
123, 7, 9co 6549 . . . . . . . . . . . . 13 class (𝑧𝑖𝑦)
135, 12wcel 1977 . . . . . . . . . . . 12 wff 𝑥 ∈ (𝑧𝑖𝑦)
145, 3, 9co 6549 . . . . . . . . . . . . 13 class (𝑥𝑖𝑧)
157, 14wcel 1977 . . . . . . . . . . . 12 wff 𝑦 ∈ (𝑥𝑖𝑧)
1611, 13, 15w3o 1030 . . . . . . . . . . 11 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
1716wn 3 . . . . . . . . . 10 wff ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
18 vp . . . . . . . . . . 11 setvar 𝑝
1918cv 1474 . . . . . . . . . 10 class 𝑝
2017, 2, 19wrex 2897 . . . . . . . . 9 wff 𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
2120, 6, 19wrex 2897 . . . . . . . 8 wff 𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
2221, 4, 19wrex 2897 . . . . . . 7 wff 𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
23 vu . . . . . . . . . . . . . . . . . 18 setvar 𝑢
2423cv 1474 . . . . . . . . . . . . . . . . 17 class 𝑢
25 vd . . . . . . . . . . . . . . . . . 18 setvar 𝑑
2625cv 1474 . . . . . . . . . . . . . . . . 17 class 𝑑
275, 24, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑥𝑑𝑢)
28 vv . . . . . . . . . . . . . . . . . 18 setvar 𝑣
2928cv 1474 . . . . . . . . . . . . . . . . 17 class 𝑣
305, 29, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑥𝑑𝑣)
3127, 30wceq 1475 . . . . . . . . . . . . . . 15 wff (𝑥𝑑𝑢) = (𝑥𝑑𝑣)
327, 24, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑦𝑑𝑢)
337, 29, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑦𝑑𝑣)
3432, 33wceq 1475 . . . . . . . . . . . . . . 15 wff (𝑦𝑑𝑢) = (𝑦𝑑𝑣)
353, 24, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑧𝑑𝑢)
363, 29, 26co 6549 . . . . . . . . . . . . . . . 16 class (𝑧𝑑𝑣)
3735, 36wceq 1475 . . . . . . . . . . . . . . 15 wff (𝑧𝑑𝑢) = (𝑧𝑑𝑣)
3831, 34, 37w3a 1031 . . . . . . . . . . . . . 14 wff ((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣))
3924, 29wne 2780 . . . . . . . . . . . . . 14 wff 𝑢𝑣
4038, 39wa 383 . . . . . . . . . . . . 13 wff (((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣)
4140, 16wi 4 . . . . . . . . . . . 12 wff ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4241, 28, 19wral 2896 . . . . . . . . . . 11 wff 𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4342, 23, 19wral 2896 . . . . . . . . . 10 wff 𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4443, 2, 19wral 2896 . . . . . . . . 9 wff 𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4544, 6, 19wral 2896 . . . . . . . 8 wff 𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4645, 4, 19wral 2896 . . . . . . 7 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)))
4722, 46wa 383 . . . . . 6 wff (∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
48 vf . . . . . . . 8 setvar 𝑓
4948cv 1474 . . . . . . 7 class 𝑓
50 citv 25135 . . . . . . 7 class Itv
5149, 50cfv 5804 . . . . . 6 class (Itv‘𝑓)
5247, 8, 51wsbc 3402 . . . . 5 wff [(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
53 cds 15777 . . . . . 6 class dist
5449, 53cfv 5804 . . . . 5 class (dist‘𝑓)
5552, 25, 54wsbc 3402 . . . 4 wff [(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
56 cbs 15695 . . . . 5 class Base
5749, 56cfv 5804 . . . 4 class (Base‘𝑓)
5855, 18, 57wsbc 3402 . . 3 wff [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))
5958, 48cab 2596 . 2 class {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
601, 59wceq 1475 1 wff TarskiG2D = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∃𝑥𝑝𝑦𝑝𝑧𝑝 ¬ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((((𝑥𝑑𝑢) = (𝑥𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑢) = (𝑧𝑑𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkg2d  29997
  Copyright terms: Public domain W3C validator