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

Definition df-trkgcb 22916
Description: Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.)
Assertion
Ref Expression
df-trkgcb  |- TarskiGCB  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )  /\  (
( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) ) ) )  ->  ( z
d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  (
y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) ) }
Distinct variable group:    a, b, c, d, f, p, i, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkgcb
StepHypRef Expression
1 cstrkgcb 22897 . 2  class TarskiGCB
2 vx . . . . . . . . . . . . . . . . . . . 20  setvar  x
32cv 1368 . . . . . . . . . . . . . . . . . . 19  class  x
4 vy . . . . . . . . . . . . . . . . . . . 20  setvar  y
54cv 1368 . . . . . . . . . . . . . . . . . . 19  class  y
63, 5wne 2611 . . . . . . . . . . . . . . . . . 18  wff  x  =/=  y
7 vz . . . . . . . . . . . . . . . . . . . . 21  setvar  z
87cv 1368 . . . . . . . . . . . . . . . . . . . 20  class  z
9 vi . . . . . . . . . . . . . . . . . . . . 21  setvar  i
109cv 1368 . . . . . . . . . . . . . . . . . . . 20  class  i
113, 8, 10co 6096 . . . . . . . . . . . . . . . . . . 19  class  ( x i z )
125, 11wcel 1756 . . . . . . . . . . . . . . . . . 18  wff  y  e.  ( x i z )
13 vb . . . . . . . . . . . . . . . . . . . 20  setvar  b
1413cv 1368 . . . . . . . . . . . . . . . . . . 19  class  b
15 va . . . . . . . . . . . . . . . . . . . . 21  setvar  a
1615cv 1368 . . . . . . . . . . . . . . . . . . . 20  class  a
17 vc . . . . . . . . . . . . . . . . . . . . 21  setvar  c
1817cv 1368 . . . . . . . . . . . . . . . . . . . 20  class  c
1916, 18, 10co 6096 . . . . . . . . . . . . . . . . . . 19  class  ( a i c )
2014, 19wcel 1756 . . . . . . . . . . . . . . . . . 18  wff  b  e.  ( a i c )
216, 12, 20w3a 965 . . . . . . . . . . . . . . . . 17  wff  ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )
22 vd . . . . . . . . . . . . . . . . . . . . . 22  setvar  d
2322cv 1368 . . . . . . . . . . . . . . . . . . . . 21  class  d
243, 5, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( x d y )
2516, 14, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( a d b )
2624, 25wceq 1369 . . . . . . . . . . . . . . . . . . 19  wff  ( x d y )  =  ( a d b )
275, 8, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( y d z )
2814, 18, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( b d c )
2927, 28wceq 1369 . . . . . . . . . . . . . . . . . . 19  wff  ( y d z )  =  ( b d c )
3026, 29wa 369 . . . . . . . . . . . . . . . . . 18  wff  ( ( x d y )  =  ( a d b )  /\  (
y d z )  =  ( b d c ) )
31 vu . . . . . . . . . . . . . . . . . . . . . 22  setvar  u
3231cv 1368 . . . . . . . . . . . . . . . . . . . . 21  class  u
333, 32, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( x d u )
34 vv . . . . . . . . . . . . . . . . . . . . . 22  setvar  v
3534cv 1368 . . . . . . . . . . . . . . . . . . . . 21  class  v
3616, 35, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( a d v )
3733, 36wceq 1369 . . . . . . . . . . . . . . . . . . 19  wff  ( x d u )  =  ( a d v )
385, 32, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( y d u )
3914, 35, 23co 6096 . . . . . . . . . . . . . . . . . . . 20  class  ( b d v )
4038, 39wceq 1369 . . . . . . . . . . . . . . . . . . 19  wff  ( y d u )  =  ( b d v )
4137, 40wa 369 . . . . . . . . . . . . . . . . . 18  wff  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) )
4230, 41wa 369 . . . . . . . . . . . . . . . . 17  wff  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) )
4321, 42wa 369 . . . . . . . . . . . . . . . 16  wff  ( ( x  =/=  y  /\  y  e.  ( x
i z )  /\  b  e.  ( a
i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  (
y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )
448, 32, 23co 6096 . . . . . . . . . . . . . . . . 17  class  ( z d u )
4518, 35, 23co 6096 . . . . . . . . . . . . . . . . 17  class  ( c d v )
4644, 45wceq 1369 . . . . . . . . . . . . . . . 16  wff  ( z d u )  =  ( c d v )
4743, 46wi 4 . . . . . . . . . . . . . . 15  wff  ( ( ( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
48 vp . . . . . . . . . . . . . . . 16  setvar  p
4948cv 1368 . . . . . . . . . . . . . . 15  class  p
5047, 34, 49wral 2720 . . . . . . . . . . . . . 14  wff  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5150, 17, 49wral 2720 . . . . . . . . . . . . 13  wff  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5251, 13, 49wral 2720 . . . . . . . . . . . 12  wff  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5352, 15, 49wral 2720 . . . . . . . . . . 11  wff  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5453, 31, 49wral 2720 . . . . . . . . . 10  wff  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5554, 7, 49wral 2720 . . . . . . . . 9  wff  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5655, 4, 49wral 2720 . . . . . . . 8  wff  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5756, 2, 49wral 2720 . . . . . . 7  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( (
( x  =/=  y  /\  y  e.  (
x i z )  /\  b  e.  ( a i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  ->  ( z d u )  =  ( c d v ) )
5827, 25wceq 1369 . . . . . . . . . . . . 13  wff  ( y d z )  =  ( a d b )
5912, 58wa 369 . . . . . . . . . . . 12  wff  ( y  e.  ( x i z )  /\  (
y d z )  =  ( a d b ) )
6059, 7, 49wrex 2721 . . . . . . . . . . 11  wff  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) )
6160, 13, 49wral 2720 . . . . . . . . . 10  wff  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) )
6261, 15, 49wral 2720 . . . . . . . . 9  wff  A. a  e.  p  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) )
6362, 4, 49wral 2720 . . . . . . . 8  wff  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) )
6463, 2, 49wral 2720 . . . . . . 7  wff  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) )
6557, 64wa 369 . . . . . 6  wff  ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  (
( ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )  /\  (
( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) ) ) )  ->  ( z
d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  (
y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) )
66 vf . . . . . . . 8  setvar  f
6766cv 1368 . . . . . . 7  class  f
68 citv 22902 . . . . . . 7  class Itv
6967, 68cfv 5423 . . . . . 6  class  (Itv `  f )
7065, 9, 69wsbc 3191 . . . . 5  wff  [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x
i z )  /\  b  e.  ( a
i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  (
y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  -> 
( z d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) )
71 cds 14252 . . . . . 6  class  dist
7267, 71cfv 5423 . . . . 5  class  ( dist `  f )
7370, 22, 72wsbc 3191 . . . 4  wff  [. ( dist `  f )  / 
d ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x
i z )  /\  b  e.  ( a
i c ) )  /\  ( ( ( x d y )  =  ( a d b )  /\  (
y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  ( y d u )  =  ( b d v ) ) ) )  -> 
( z d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  ( y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) )
74 cbs 14179 . . . . 5  class  Base
7567, 74cfv 5423 . . . 4  class  ( Base `  f )
7673, 48, 75wsbc 3191 . . 3  wff  [. ( Base `  f )  /  p ]. [. ( dist `  f )  /  d ]. [. (Itv `  f
)  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )  /\  (
( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) ) ) )  ->  ( z
d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  (
y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) )
7776, 66cab 2429 . 2  class  { f  |  [. ( Base `  f )  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )  /\  (
( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) ) ) )  ->  ( z
d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  (
y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) ) }
781, 77wceq 1369 1  wff TarskiGCB  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. a  e.  p  A. b  e.  p  A. c  e.  p  A. v  e.  p  ( ( ( x  =/=  y  /\  y  e.  ( x i z )  /\  b  e.  ( a i c ) )  /\  (
( ( x d y )  =  ( a d b )  /\  ( y d z )  =  ( b d c ) )  /\  ( ( x d u )  =  ( a d v )  /\  (
y d u )  =  ( b d v ) ) ) )  ->  ( z
d u )  =  ( c d v ) )  /\  A. x  e.  p  A. y  e.  p  A. a  e.  p  A. b  e.  p  E. z  e.  p  (
y  e.  ( x i z )  /\  ( y d z )  =  ( a d b ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  istrkgcb  22924
  Copyright terms: Public domain W3C validator