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

Definition df-trkgc 23600
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 2493, 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 23582 . 2  class TarskiGC
2 vx . . . . . . . . . . 11  setvar  x
32cv 1378 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  setvar  y
54cv 1378 . . . . . . . . . 10  class  y
6 vd . . . . . . . . . . 11  setvar  d
76cv 1378 . . . . . . . . . 10  class  d
83, 5, 7co 6284 . . . . . . . . 9  class  ( x d y )
95, 3, 7co 6284 . . . . . . . . 9  class  ( y d x )
108, 9wceq 1379 . . . . . . . 8  wff  ( x d y )  =  ( y d x )
11 vp . . . . . . . . 9  setvar  p
1211cv 1378 . . . . . . . 8  class  p
1310, 4, 12wral 2814 . . . . . . 7  wff  A. y  e.  p  ( x
d y )  =  ( y d x )
1413, 2, 12wral 2814 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  ( x
d y )  =  ( y d x )
15 vz . . . . . . . . . . . . 13  setvar  z
1615cv 1378 . . . . . . . . . . . 12  class  z
1716, 16, 7co 6284 . . . . . . . . . . 11  class  ( z d z )
188, 17wceq 1379 . . . . . . . . . 10  wff  ( x d y )  =  ( z d z )
192, 4weq 1705 . . . . . . . . . 10  wff  x  =  y
2018, 19wi 4 . . . . . . . . 9  wff  ( ( x d y )  =  ( z d z )  ->  x  =  y )
2120, 15, 12wral 2814 . . . . . . . 8  wff  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2221, 4, 12wral 2814 . . . . . . 7  wff  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2322, 2, 12wral 2814 . . . . . 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 1378 . . . . . 6  class  f
27 cds 14564 . . . . . 6  class  dist
2826, 27cfv 5588 . . . . 5  class  ( dist `  f )
2924, 6, 28wsbc 3331 . . . 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 14490 . . . . 5  class  Base
3126, 30cfv 5588 . . . 4  class  ( Base `  f )
3229, 11, 31wsbc 3331 . . 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 2452 . 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 1379 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  23607
  Copyright terms: Public domain W3C validator