Metamath Proof Explorer

Definition df-trkge

Description: Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of Schwabhauser p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Assertion df-trkge 
|- TarskiGE = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkge 
 |-  TarskiGE
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 vz 
 |-  z
13 vu 
 |-  u
14 vv 
 |-  v
15 13 cv 
 |-  u
16 9 cv 
 |-  x
17 8 cv 
 |-  i
18 14 cv 
 |-  v
19 16 18 17 co 
 |-  ( x i v )
20 15 19 wcel 
 |-  u e. ( x i v )
21 11 cv 
 |-  y
22 12 cv 
 |-  z
23 21 22 17 co 
 |-  ( y i z )
24 15 23 wcel 
 |-  u e. ( y i z )
25 16 15 wne 
 |-  x =/= u
26 20 24 25 w3a 
 |-  ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u )
27 va 
 |-  a
28 vb 
 |-  b
29 27 cv 
 |-  a
30 16 29 17 co 
 |-  ( x i a )
31 21 30 wcel 
 |-  y e. ( x i a )
32 28 cv 
 |-  b
33 16 32 17 co 
 |-  ( x i b )
34 22 33 wcel 
 |-  z e. ( x i b )
35 29 32 17 co 
 |-  ( a i b )
36 18 35 wcel 
 |-  v e. ( a i b )
37 31 34 36 w3a 
 |-  ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
38 37 28 10 wrex 
 |-  E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
39 38 27 10 wrex 
 |-  E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
40 26 39 wi 
 |-  ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
41 40 14 10 wral 
 |-  A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
42 41 13 10 wral 
 |-  A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
43 42 12 10 wral 
 |-  A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
46 45 8 7 wsbc 
 |-  [. ( Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
47 46 5 4 wsbc 
 |-  [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
48 47 1 cab 
 |-  { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }
49 0 48 wceq 
 |-  TarskiGE = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }