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

Definition df-trkgc 22921
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 2460, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.)
Assertion
Ref Expression
df-trkgc  |- TarskiGC  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. ( A. x  e.  p  A. y  e.  p  ( x d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  (
( x d y )  =  ( z d z )  ->  x  =  y )
) }
Distinct variable group:    f, d, p, x, y, z

Detailed syntax breakdown of Definition df-trkgc
StepHypRef Expression
1 cstrkgc 22902 . 2  class TarskiGC
2 vx . . . . . . . . . . 11  setvar  x
32cv 1368 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  setvar  y
54cv 1368 . . . . . . . . . 10  class  y
6 vd . . . . . . . . . . 11  setvar  d
76cv 1368 . . . . . . . . . 10  class  d
83, 5, 7co 6103 . . . . . . . . 9  class  ( x d y )
95, 3, 7co 6103 . . . . . . . . 9  class  ( y d x )
108, 9wceq 1369 . . . . . . . 8  wff  ( x d y )  =  ( y d x )
11 vp . . . . . . . . 9  setvar  p
1211cv 1368 . . . . . . . 8  class  p
1310, 4, 12wral 2727 . . . . . . 7  wff  A. y  e.  p  ( x
d y )  =  ( y d x )
1413, 2, 12wral 2727 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  ( x
d y )  =  ( y d x )
15 vz . . . . . . . . . . . . 13  setvar  z
1615cv 1368 . . . . . . . . . . . 12  class  z
1716, 16, 7co 6103 . . . . . . . . . . 11  class  ( z d z )
188, 17wceq 1369 . . . . . . . . . 10  wff  ( x d y )  =  ( z d z )
192, 4weq 1695 . . . . . . . . . 10  wff  x  =  y
2018, 19wi 4 . . . . . . . . 9  wff  ( ( x d y )  =  ( z d z )  ->  x  =  y )
2120, 15, 12wral 2727 . . . . . . . 8  wff  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2221, 4, 12wral 2727 . . . . . . 7  wff  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2322, 2, 12wral 2727 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2414, 23wa 369 . . . . 5  wff  ( A. x  e.  p  A. y  e.  p  (
x d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  (
( x d y )  =  ( z d z )  ->  x  =  y )
)
25 vf . . . . . . 7  setvar  f
2625cv 1368 . . . . . 6  class  f
27 cds 14259 . . . . . 6  class  dist
2826, 27cfv 5430 . . . . 5  class  ( dist `  f )
2924, 6, 28wsbc 3198 . . . 4  wff  [. ( dist `  f )  / 
d ]. ( A. x  e.  p  A. y  e.  p  ( x
d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y ) )
30 cbs 14186 . . . . 5  class  Base
3126, 30cfv 5430 . . . 4  class  ( Base `  f )
3229, 11, 31wsbc 3198 . . 3  wff  [. ( Base `  f )  /  p ]. [. ( dist `  f )  /  d ]. ( A. x  e.  p  A. y  e.  p  ( x d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  ( ( x d y )  =  ( z d z )  ->  x  =  y ) )
3332, 25cab 2429 . 2  class  { f  |  [. ( Base `  f )  /  p ]. [. ( dist `  f
)  /  d ]. ( A. x  e.  p  A. y  e.  p  ( x d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  (
( x d y )  =  ( z d z )  ->  x  =  y )
) }
341, 33wceq 1369 1  wff TarskiGC  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. ( A. x  e.  p  A. y  e.  p  ( x d y )  =  ( y d x )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  (
( x d y )  =  ( z d z )  ->  x  =  y )
) }
Colors of variables: wff setvar class
This definition is referenced by:  istrkgc  22929
  Copyright terms: Public domain W3C validator