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

Definition df-trkgc 24438
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 2447, 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 24421 . 2  class TarskiGC
2 vx . . . . . . . . . . 11  setvar  x
32cv 1436 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  setvar  y
54cv 1436 . . . . . . . . . 10  class  y
6 vd . . . . . . . . . . 11  setvar  d
76cv 1436 . . . . . . . . . 10  class  d
83, 5, 7co 6249 . . . . . . . . 9  class  ( x d y )
95, 3, 7co 6249 . . . . . . . . 9  class  ( y d x )
108, 9wceq 1437 . . . . . . . 8  wff  ( x d y )  =  ( y d x )
11 vp . . . . . . . . 9  setvar  p
1211cv 1436 . . . . . . . 8  class  p
1310, 4, 12wral 2714 . . . . . . 7  wff  A. y  e.  p  ( x
d y )  =  ( y d x )
1413, 2, 12wral 2714 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  ( x
d y )  =  ( y d x )
15 vz . . . . . . . . . . . . 13  setvar  z
1615cv 1436 . . . . . . . . . . . 12  class  z
1716, 16, 7co 6249 . . . . . . . . . . 11  class  ( z d z )
188, 17wceq 1437 . . . . . . . . . 10  wff  ( x d y )  =  ( z d z )
192, 4weq 1784 . . . . . . . . . 10  wff  x  =  y
2018, 19wi 4 . . . . . . . . 9  wff  ( ( x d y )  =  ( z d z )  ->  x  =  y )
2120, 15, 12wral 2714 . . . . . . . 8  wff  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2221, 4, 12wral 2714 . . . . . . 7  wff  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2322, 2, 12wral 2714 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  ( (
x d y )  =  ( z d z )  ->  x  =  y )
2414, 23wa 370 . . . . 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 1436 . . . . . 6  class  f
27 cds 15142 . . . . . 6  class  dist
2826, 27cfv 5544 . . . . 5  class  ( dist `  f )
2924, 6, 28wsbc 3242 . . . 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 15064 . . . . 5  class  Base
3126, 30cfv 5544 . . . 4  class  ( Base `  f )
3229, 11, 31wsbc 3242 . . 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 2414 . 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 1437 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  24444
  Copyright terms: Public domain W3C validator