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

Definition df-trkgc 26245
Description: Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2821, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.)
Assertion
Ref Expression
df-trkgc TarskiGC = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}
Distinct variable group:   𝑓,𝑑,𝑝,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgc
StepHypRef Expression
1 cstrkgc 26228 . 2 class TarskiGC
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1537 . . . . . . . . . 10 class 𝑥
4 vy . . . . . . . . . . 11 setvar 𝑦
54cv 1537 . . . . . . . . . 10 class 𝑦
6 vd . . . . . . . . . . 11 setvar 𝑑
76cv 1537 . . . . . . . . . 10 class 𝑑
83, 5, 7co 7139 . . . . . . . . 9 class (𝑥𝑑𝑦)
95, 3, 7co 7139 . . . . . . . . 9 class (𝑦𝑑𝑥)
108, 9wceq 1538 . . . . . . . 8 wff (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
11 vp . . . . . . . . 9 setvar 𝑝
1211cv 1537 . . . . . . . 8 class 𝑝
1310, 4, 12wral 3109 . . . . . . 7 wff 𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
1413, 2, 12wral 3109 . . . . . 6 wff 𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
15 vz . . . . . . . . . . . . 13 setvar 𝑧
1615cv 1537 . . . . . . . . . . . 12 class 𝑧
1716, 16, 7co 7139 . . . . . . . . . . 11 class (𝑧𝑑𝑧)
188, 17wceq 1538 . . . . . . . . . 10 wff (𝑥𝑑𝑦) = (𝑧𝑑𝑧)
192, 4weq 1964 . . . . . . . . . 10 wff 𝑥 = 𝑦
2018, 19wi 4 . . . . . . . . 9 wff ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
2120, 15, 12wral 3109 . . . . . . . 8 wff 𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
2221, 4, 12wral 3109 . . . . . . 7 wff 𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
2322, 2, 12wral 3109 . . . . . 6 wff 𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
2414, 23wa 399 . . . . 5 wff (∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
25 vf . . . . . . 7 setvar 𝑓
2625cv 1537 . . . . . 6 class 𝑓
27 cds 16569 . . . . . 6 class dist
2826, 27cfv 6328 . . . . 5 class (dist‘𝑓)
2924, 6, 28wsbc 3723 . . . 4 wff [(dist‘𝑓) / 𝑑](∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
30 cbs 16478 . . . . 5 class Base
3126, 30cfv 6328 . . . 4 class (Base‘𝑓)
3229, 11, 31wsbc 3723 . . 3 wff [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
3332, 25cab 2779 . 2 class {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}
341, 33wceq 1538 1 wff TarskiGC = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥𝑝𝑦𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgc  26251
  Copyright terms: Public domain W3C validator