Metamath Proof Explorer

Definition df-trkgb

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgb 
 |-  TarskiGB
1 vf 
 |-  f
2 cbs 
 |-  Base
3 1 cv 
 |-  f
4 3 2 cfv 
 |-  ( Base ` f )
5 vp 
 |-  p
6 citv 
 |-  Itv
7 3 6 cfv 
 |-  ( Itv ` f )
8 vi 
 |-  i
9 vx 
 |-  x
10 5 cv 
 |-  p
11 vy 
 |-  y
12 11 cv 
 |-  y
13 9 cv 
 |-  x
14 8 cv 
 |-  i
15 13 13 14 co 
 |-  ( x i x )
16 12 15 wcel 
 |-  y e. ( x i x )
17 13 12 wceq 
 |-  x = y
18 16 17 wi 
 |-  ( y e. ( x i x ) -> x = y )
19 18 11 10 wral 
 |-  A. y e. p ( y e. ( x i x ) -> x = y )
20 19 9 10 wral 
 |-  A. x e. p A. y e. p ( y e. ( x i x ) -> x = y )
21 vz 
 |-  z
22 vu 
 |-  u
23 vv 
 |-  v
24 22 cv 
 |-  u
25 21 cv 
 |-  z
26 13 25 14 co 
 |-  ( x i z )
27 24 26 wcel 
 |-  u e. ( x i z )
28 23 cv 
 |-  v
29 12 25 14 co 
 |-  ( y i z )
30 28 29 wcel 
 |-  v e. ( y i z )
31 27 30 wa 
 |-  ( u e. ( x i z ) /\ v e. ( y i z ) )
32 va 
 |-  a
33 32 cv 
 |-  a
34 24 12 14 co 
 |-  ( u i y )
35 33 34 wcel 
 |-  a e. ( u i y )
36 28 13 14 co 
 |-  ( v i x )
37 33 36 wcel 
 |-  a e. ( v i x )
38 35 37 wa 
 |-  ( a e. ( u i y ) /\ a e. ( v i x ) )
39 38 32 10 wrex 
 |-  E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) )
40 31 39 wi 
 |-  ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
41 40 23 10 wral 
 |-  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 ) ) )
42 41 22 10 wral 
 |-  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 ) ) )
43 42 21 10 wral 
 |-  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 ) ) )
44 43 11 10 wral 
 |-  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 ) ) )
45 44 9 10 wral 
 |-  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 ) ) )
46 vs 
 |-  s
47 10 cpw 
 |-  ~P p
48 vt 
 |-  t
49 46 cv 
 |-  s
50 48 cv 
 |-  t
51 33 12 14 co 
 |-  ( a i y )
52 13 51 wcel 
 |-  x e. ( a i y )
53 52 11 50 wral 
 |-  A. y e. t x e. ( a i y )
54 53 9 49 wral 
 |-  A. x e. s A. y e. t x e. ( a i y )
55 54 32 10 wrex 
 |-  E. a e. p A. x e. s A. y e. t x e. ( a i y )
56 vb 
 |-  b
57 56 cv 
 |-  b
58 13 12 14 co 
 |-  ( x i y )
59 57 58 wcel 
 |-  b e. ( x i y )
60 59 11 50 wral 
 |-  A. y e. t b e. ( x i y )
61 60 9 49 wral 
 |-  A. x e. s A. y e. t b e. ( x i y )
62 61 56 10 wrex 
 |-  E. b e. p A. x e. s A. y e. t b e. ( x i y )
63 55 62 wi 
 |-  ( 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 ) )
64 63 48 47 wral 
 |-  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 ) )
65 64 46 47 wral 
 |-  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 ) )
66 20 45 65 w3a 
 |-  ( 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 66 8 7 wsbc 
 |-  [. ( 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 ) ) )
68 67 5 4 wsbc 
 |-  [. ( 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 ) ) )
69 68 1 cab 
 |-  { 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 ) ) ) }
70 0 69 wceq 
 |-  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 ) ) ) }