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

Definition df-trkgb 22929
Description: Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.)
Assertion
Ref Expression
df-trkgb  |- TarskiGB  =  { f  |  [. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) ) }
Distinct variable group:    a, b, f, p, i, s, t, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkgb
StepHypRef Expression
1 cstrkgb 22910 . 2  class TarskiGB
2 vy . . . . . . . . . . 11  setvar  y
32cv 1368 . . . . . . . . . 10  class  y
4 vx . . . . . . . . . . . 12  setvar  x
54cv 1368 . . . . . . . . . . 11  class  x
6 vi . . . . . . . . . . . 12  setvar  i
76cv 1368 . . . . . . . . . . 11  class  i
85, 5, 7co 6110 . . . . . . . . . 10  class  ( x i x )
93, 8wcel 1756 . . . . . . . . 9  wff  y  e.  ( x i x )
104, 2weq 1695 . . . . . . . . 9  wff  x  =  y
119, 10wi 4 . . . . . . . 8  wff  ( y  e.  ( x i x )  ->  x  =  y )
12 vp . . . . . . . . 9  setvar  p
1312cv 1368 . . . . . . . 8  class  p
1411, 2, 13wral 2734 . . . . . . 7  wff  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )
1514, 4, 13wral 2734 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )
16 vu . . . . . . . . . . . . . . 15  setvar  u
1716cv 1368 . . . . . . . . . . . . . 14  class  u
18 vz . . . . . . . . . . . . . . . 16  setvar  z
1918cv 1368 . . . . . . . . . . . . . . 15  class  z
205, 19, 7co 6110 . . . . . . . . . . . . . 14  class  ( x i z )
2117, 20wcel 1756 . . . . . . . . . . . . 13  wff  u  e.  ( x i z )
22 vv . . . . . . . . . . . . . . 15  setvar  v
2322cv 1368 . . . . . . . . . . . . . 14  class  v
243, 19, 7co 6110 . . . . . . . . . . . . . 14  class  ( y i z )
2523, 24wcel 1756 . . . . . . . . . . . . 13  wff  v  e.  ( y i z )
2621, 25wa 369 . . . . . . . . . . . 12  wff  ( u  e.  ( x i z )  /\  v  e.  ( y i z ) )
27 va . . . . . . . . . . . . . . . 16  setvar  a
2827cv 1368 . . . . . . . . . . . . . . 15  class  a
2917, 3, 7co 6110 . . . . . . . . . . . . . . 15  class  ( u i y )
3028, 29wcel 1756 . . . . . . . . . . . . . 14  wff  a  e.  ( u i y )
3123, 5, 7co 6110 . . . . . . . . . . . . . . 15  class  ( v i x )
3228, 31wcel 1756 . . . . . . . . . . . . . 14  wff  a  e.  ( v i x )
3330, 32wa 369 . . . . . . . . . . . . 13  wff  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) )
3433, 27, 13wrex 2735 . . . . . . . . . . . 12  wff  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) )
3526, 34wi 4 . . . . . . . . . . 11  wff  ( ( u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
3635, 22, 13wral 2734 . . . . . . . . . 10  wff  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
3736, 16, 13wral 2734 . . . . . . . . 9  wff  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
3837, 18, 13wral 2734 . . . . . . . 8  wff  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
3938, 2, 13wral 2734 . . . . . . 7  wff  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
4039, 4, 13wral 2734 . . . . . 6  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )
4128, 3, 7co 6110 . . . . . . . . . . . . 13  class  ( a i y )
425, 41wcel 1756 . . . . . . . . . . . 12  wff  x  e.  ( a i y )
43 vt . . . . . . . . . . . . 13  setvar  t
4443cv 1368 . . . . . . . . . . . 12  class  t
4542, 2, 44wral 2734 . . . . . . . . . . 11  wff  A. y  e.  t  x  e.  ( a i y )
46 vs . . . . . . . . . . . 12  setvar  s
4746cv 1368 . . . . . . . . . . 11  class  s
4845, 4, 47wral 2734 . . . . . . . . . 10  wff  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )
4948, 27, 13wrex 2735 . . . . . . . . 9  wff  E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )
50 vb . . . . . . . . . . . . . 14  setvar  b
5150cv 1368 . . . . . . . . . . . . 13  class  b
525, 3, 7co 6110 . . . . . . . . . . . . 13  class  ( x i y )
5351, 52wcel 1756 . . . . . . . . . . . 12  wff  b  e.  ( x i y )
5453, 2, 44wral 2734 . . . . . . . . . . 11  wff  A. y  e.  t  b  e.  ( x i y )
5554, 4, 47wral 2734 . . . . . . . . . 10  wff  A. x  e.  s  A. y  e.  t  b  e.  ( x i y )
5655, 50, 13wrex 2735 . . . . . . . . 9  wff  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y )
5749, 56wi 4 . . . . . . . 8  wff  ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) )
5813cpw 3879 . . . . . . . 8  class  ~P p
5957, 43, 58wral 2734 . . . . . . 7  wff  A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) )
6059, 46, 58wral 2734 . . . . . 6  wff  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) )
6115, 40, 60w3a 965 . . . . 5  wff  ( A. x  e.  p  A. y  e.  p  (
y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( ( u  e.  ( x i z )  /\  v  e.  ( y i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) )
62 vf . . . . . . 7  setvar  f
6362cv 1368 . . . . . 6  class  f
64 citv 22916 . . . . . 6  class Itv
6563, 64cfv 5437 . . . . 5  class  (Itv `  f )
6661, 6, 65wsbc 3205 . . . 4  wff  [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  (
( u  e.  ( x i z )  /\  v  e.  ( y i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) )
67 cbs 14193 . . . . 5  class  Base
6863, 67cfv 5437 . . . 4  class  ( Base `  f )
6966, 12, 68wsbc 3205 . . 3  wff  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  (
( u  e.  ( x i z )  /\  v  e.  ( y i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) )
7069, 62cab 2429 . 2  class  { f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f
)  /  i ]. ( A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) ) }
711, 70wceq 1369 1  wff TarskiGB  =  { f  |  [. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. ( A. x  e.  p  A. y  e.  p  ( y  e.  ( x i x )  ->  x  =  y )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
u  e.  ( x i z )  /\  v  e.  ( y
i z ) )  ->  E. a  e.  p  ( a  e.  ( u i y )  /\  a  e.  ( v i x ) ) )  /\  A. s  e.  ~P  p A. t  e.  ~P  p ( E. a  e.  p  A. x  e.  s  A. y  e.  t  x  e.  ( a i y )  ->  E. b  e.  p  A. x  e.  s  A. y  e.  t  b  e.  ( x i y ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  istrkgb  22937
  Copyright terms: Public domain W3C validator