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

Definition df-trkgc 24045
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 2480, 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 24027 . 2  class TarskiGC
2 vx . . . . . . . . . . 11  setvar  x
32cv 1397 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  setvar  y
54cv 1397 . . . . . . . . . 10  class  y
6 vd . . . . . . . . . . 11  setvar  d
76cv 1397 . . . . . . . . . 10  class  d
83, 5, 7co 6270 . . . . . . . . 9  class  ( x d y )
95, 3, 7co 6270 . . . . . . . . 9  class  ( y d x )
108, 9wceq 1398 . . . . . . . 8  wff  ( x d y )  =  ( y d x )
11 vp . . . . . . . . 9  setvar  p
1211cv 1397 . . . . . . . 8  class  p
1310, 4, 12wral 2804 . . . . . . 7  wff  A. y  e.  p  ( x
d y )  =  ( y d x )
1413, 2, 12wral 2804 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  ( x
d y )  =  ( y d x )
15 vz . . . . . . . . . . . . 13  setvar  z
1615cv 1397 . . . . . . . . . . . 12  class  z
1716, 16, 7co 6270 . . . . . . . . . . 11  class  ( z d z )
188, 17wceq 1398 . . . . . . . . . 10  wff  ( x d y )  =  ( z d z )
192, 4weq 1738 . . . . . . . . . 10  wff  x  =  y
2018, 19wi 4 . . . . . . . . 9  wff  ( ( x d y )  =  ( z d z )  ->  x  =  y )
2120, 15, 12wral 2804 . . . . . . . 8  wff  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2221, 4, 12wral 2804 . . . . . . 7  wff  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2322, 2, 12wral 2804 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2414, 23wa 367 . . . . 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 1397 . . . . . 6  class  f
27 cds 14796 . . . . . 6  class  dist
2826, 27cfv 5570 . . . . 5  class  ( dist `  f )
2924, 6, 28wsbc 3324 . . . 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 14719 . . . . 5  class  Base
3126, 30cfv 5570 . . . 4  class  ( Base `  f )
3229, 11, 31wsbc 3324 . . 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 2439 . 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 1398 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  24052
  Copyright terms: Public domain W3C validator