Metamath Proof Explorer

Definition df-trkg2d

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) (New usage is discouraged.)

Ref Expression
Assertion 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkg2d 
 |-  TarskiG2D
1 vf 
 |-  f
2 cbs 
 |-  Base
3 1 cv 
 |-  f
4 3 2 cfv 
 |-  ( Base ` f )
5 vp 
 |-  p
6 cds 
 |-  dist
7 3 6 cfv 
 |-  ( dist ` f )
8 vd 
 |-  d
9 citv 
 |-  Itv
10 3 9 cfv 
 |-  ( Itv ` f )
11 vi 
 |-  i
12 vx 
 |-  x
13 5 cv 
 |-  p
14 vy 
 |-  y
15 vz 
 |-  z
16 15 cv 
 |-  z
17 12 cv 
 |-  x
18 11 cv 
 |-  i
19 14 cv 
 |-  y
20 17 19 18 co 
 |-  ( x i y )
21 16 20 wcel 
 |-  z e. ( x i y )
22 16 19 18 co 
 |-  ( z i y )
23 17 22 wcel 
 |-  x e. ( z i y )
24 17 16 18 co 
 |-  ( x i z )
25 19 24 wcel 
 |-  y e. ( x i z )
26 21 23 25 w3o 
 |-  ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
27 26 wn 
 |-  -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
28 27 15 13 wrex 
 |-  E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
29 28 14 13 wrex 
 |-  E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
30 29 12 13 wrex 
 |-  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 ) )
31 vu 
 |-  u
32 vv 
 |-  v
33 8 cv 
 |-  d
34 31 cv 
 |-  u
35 17 34 33 co 
 |-  ( x d u )
36 32 cv 
 |-  v
37 17 36 33 co 
 |-  ( x d v )
38 35 37 wceq 
 |-  ( x d u ) = ( x d v )
39 19 34 33 co 
 |-  ( y d u )
40 19 36 33 co 
 |-  ( y d v )
41 39 40 wceq 
 |-  ( y d u ) = ( y d v )
42 16 34 33 co 
 |-  ( z d u )
43 16 36 33 co 
 |-  ( z d v )
44 42 43 wceq 
 |-  ( z d u ) = ( z d v )
45 38 41 44 w3a 
 |-  ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) )
46 34 36 wne 
 |-  u =/= v
47 45 46 wa 
 |-  ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v )
48 47 26 wi 
 |-  ( ( ( ( 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 ) ) )
49 48 32 13 wral 
 |-  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 ) ) )
50 49 31 13 wral 
 |-  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 ) ) )
51 50 15 13 wral 
 |-  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 ) ) )
52 51 14 13 wral 
 |-  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 52 12 13 wral 
 |-  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 ) ) )
54 30 53 wa 
 |-  ( 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 ) ) ) )
55 54 11 10 wsbc 
 |-  [. ( 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 55 8 7 wsbc 
 |-  [. ( 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 ) ) ) )
57 56 5 4 wsbc 
 |-  [. ( 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 ) ) ) )
58 57 1 cab 
 |-  { 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 ) ) ) ) }
59 0 58 wceq 
 |-  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 ) ) ) ) }