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 27737
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 2755, 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 27717 . 2 class TarskiGC
2 vx . . . . . . . . . . 11 setvar π‘₯
32cv 1540 . . . . . . . . . 10 class π‘₯
4 vy . . . . . . . . . . 11 setvar 𝑦
54cv 1540 . . . . . . . . . 10 class 𝑦
6 vd . . . . . . . . . . 11 setvar 𝑑
76cv 1540 . . . . . . . . . 10 class 𝑑
83, 5, 7co 7411 . . . . . . . . 9 class (π‘₯𝑑𝑦)
95, 3, 7co 7411 . . . . . . . . 9 class (𝑦𝑑π‘₯)
108, 9wceq 1541 . . . . . . . 8 wff (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯)
11 vp . . . . . . . . 9 setvar 𝑝
1211cv 1540 . . . . . . . 8 class 𝑝
1310, 4, 12wral 3061 . . . . . . 7 wff βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯)
1413, 2, 12wral 3061 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯)
15 vz . . . . . . . . . . . . 13 setvar 𝑧
1615cv 1540 . . . . . . . . . . . 12 class 𝑧
1716, 16, 7co 7411 . . . . . . . . . . 11 class (𝑧𝑑𝑧)
188, 17wceq 1541 . . . . . . . . . 10 wff (π‘₯𝑑𝑦) = (𝑧𝑑𝑧)
192, 4weq 1966 . . . . . . . . . 10 wff π‘₯ = 𝑦
2018, 19wi 4 . . . . . . . . 9 wff ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦)
2120, 15, 12wral 3061 . . . . . . . 8 wff βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦)
2221, 4, 12wral 3061 . . . . . . 7 wff βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦)
2322, 2, 12wral 3061 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦)
2414, 23wa 396 . . . . 5 wff (βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦))
25 vf . . . . . . 7 setvar 𝑓
2625cv 1540 . . . . . 6 class 𝑓
27 cds 17208 . . . . . 6 class dist
2826, 27cfv 6543 . . . . 5 class (distβ€˜π‘“)
2924, 6, 28wsbc 3777 . . . 4 wff [(distβ€˜π‘“) / 𝑑](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦))
30 cbs 17146 . . . . 5 class Base
3126, 30cfv 6543 . . . 4 class (Baseβ€˜π‘“)
3229, 11, 31wsbc 3777 . . 3 wff [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦))
3332, 25cab 2709 . 2 class {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦))}
341, 33wceq 1541 1 wff TarskiGC = {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (π‘₯𝑑𝑦) = (𝑦𝑑π‘₯) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 ((π‘₯𝑑𝑦) = (𝑧𝑑𝑧) β†’ π‘₯ = 𝑦))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgc  27743
  Copyright terms: Public domain W3C validator