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

Definition df-trkg2d 23974
Description: Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.)
Assertion
Ref Expression
df-trkg2d  |- TarskiG2D  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) ) }
Distinct variable group:    f, d, p, i, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkg2d
StepHypRef Expression
1 cstrkg2d 23955 . 2  class TarskiG2D
2 vz . . . . . . . . . . . . . 14  setvar  z
32cv 1394 . . . . . . . . . . . . 13  class  z
4 vx . . . . . . . . . . . . . . 15  setvar  x
54cv 1394 . . . . . . . . . . . . . 14  class  x
6 vy . . . . . . . . . . . . . . 15  setvar  y
76cv 1394 . . . . . . . . . . . . . 14  class  y
8 vi . . . . . . . . . . . . . . 15  setvar  i
98cv 1394 . . . . . . . . . . . . . 14  class  i
105, 7, 9co 6296 . . . . . . . . . . . . 13  class  ( x i y )
113, 10wcel 1819 . . . . . . . . . . . 12  wff  z  e.  ( x i y )
123, 7, 9co 6296 . . . . . . . . . . . . 13  class  ( z i y )
135, 12wcel 1819 . . . . . . . . . . . 12  wff  x  e.  ( z i y )
145, 3, 9co 6296 . . . . . . . . . . . . 13  class  ( x i z )
157, 14wcel 1819 . . . . . . . . . . . 12  wff  y  e.  ( x i z )
1611, 13, 15w3o 972 . . . . . . . . . . 11  wff  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
1716wn 3 . . . . . . . . . 10  wff  -.  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
18 vp . . . . . . . . . . 11  setvar  p
1918cv 1394 . . . . . . . . . 10  class  p
2017, 2, 19wrex 2808 . . . . . . . . 9  wff  E. z  e.  p  -.  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
2120, 6, 19wrex 2808 . . . . . . . 8  wff  E. y  e.  p  E. z  e.  p  -.  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
2221, 4, 19wrex 2808 . . . . . . 7  wff  E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
23 vu . . . . . . . . . . . . . . . . . 18  setvar  u
2423cv 1394 . . . . . . . . . . . . . . . . 17  class  u
25 vd . . . . . . . . . . . . . . . . . 18  setvar  d
2625cv 1394 . . . . . . . . . . . . . . . . 17  class  d
275, 24, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( x d u )
28 vv . . . . . . . . . . . . . . . . . 18  setvar  v
2928cv 1394 . . . . . . . . . . . . . . . . 17  class  v
305, 29, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( x d v )
3127, 30wceq 1395 . . . . . . . . . . . . . . 15  wff  ( x d u )  =  ( x d v )
327, 24, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( y d u )
337, 29, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( y d v )
3432, 33wceq 1395 . . . . . . . . . . . . . . 15  wff  ( y d u )  =  ( y d v )
353, 24, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( z d u )
363, 29, 26co 6296 . . . . . . . . . . . . . . . 16  class  ( z d v )
3735, 36wceq 1395 . . . . . . . . . . . . . . 15  wff  ( z d u )  =  ( z d v )
3831, 34, 37w3a 973 . . . . . . . . . . . . . 14  wff  ( ( x d u )  =  ( x d v )  /\  (
y d u )  =  ( y d v )  /\  (
z d u )  =  ( z d v ) )
3924, 29wne 2652 . . . . . . . . . . . . . 14  wff  u  =/=  v
4038, 39wa 369 . . . . . . . . . . . . 13  wff  ( ( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v
)
4140, 16wi 4 . . . . . . . . . . . 12  wff  ( ( ( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4241, 28, 19wral 2807 . . . . . . . . . . 11  wff  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4342, 23, 19wral 2807 . . . . . . . . . 10  wff  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4443, 2, 19wral 2807 . . . . . . . . 9  wff  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4544, 6, 19wral 2807 . . . . . . . 8  wff  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4645, 4, 19wral 2807 . . . . . . 7  wff  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) )
4722, 46wa 369 . . . . . 6  wff  ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
48 vf . . . . . . . 8  setvar  f
4948cv 1394 . . . . . . 7  class  f
50 citv 23957 . . . . . . 7  class Itv
5149, 50cfv 5594 . . . . . 6  class  (Itv `  f )
5247, 8, 51wsbc 3327 . . . . 5  wff  [. (Itv `  f )  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  (
( ( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
53 cds 14720 . . . . . 6  class  dist
5449, 53cfv 5594 . . . . 5  class  ( dist `  f )
5552, 25, 54wsbc 3327 . . . 4  wff  [. ( dist `  f )  / 
d ]. [. (Itv `  f )  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  (
( ( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
56 cbs 14643 . . . . 5  class  Base
5749, 56cfv 5594 . . . 4  class  ( Base `  f )
5855, 18, 57wsbc 3327 . . 3  wff  [. ( Base `  f )  /  p ]. [. ( dist `  f )  /  d ]. [. (Itv `  f
)  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) )
5958, 48cab 2442 . 2  class  { f  |  [. ( Base `  f )  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) ) }
601, 59wceq 1395 1  wff TarskiG2D  =  { f  |  [. ( Base `  f
)  /  p ]. [. ( dist `  f
)  /  d ]. [. (Itv `  f )  /  i ]. ( E. x  e.  p  E. y  e.  p  E. z  e.  p  -.  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )  /\  A. x  e.  p  A. y  e.  p  A. z  e.  p  A. u  e.  p  A. v  e.  p  ( (
( ( x d u )  =  ( x d v )  /\  ( y d u )  =  ( y d v )  /\  ( z d u )  =  ( z d v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  istrkg2d  23981
  Copyright terms: Public domain W3C validator