Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-neug Unicode version

Definition df-neug 25363
Description: Definition of a neutral geometry. Every Dedekind cut of a line has a cut point. (Axiom of Dedekind in [AitkenNG] p. 3.) (For my private use only. Don't use.) (Contributed by FL, 1-Apr-2016.)
Assertion
Ref Expression
df-neug  |- Neug  =  {
g  e. Ibcg  |  A. l  e.  (PLines `  g
) A. u  e.  ( (slices `  g
) `  l )
( ( 1st `  u
) (Cut `  g
) ( 2nd `  u
) )  =/=  (/) }
Distinct variable group:    g, l, u

Detailed syntax breakdown of Definition df-neug
StepHypRef Expression
1 cneug 25362 . 2  class Neug
2 vu . . . . . . . . 9  set  u
32cv 1618 . . . . . . . 8  class  u
4 c1st 5972 . . . . . . . 8  class  1st
53, 4cfv 4592 . . . . . . 7  class  ( 1st `  u )
6 c2nd 5973 . . . . . . . 8  class  2nd
73, 6cfv 4592 . . . . . . 7  class  ( 2nd `  u )
8 vg . . . . . . . . 9  set  g
98cv 1618 . . . . . . . 8  class  g
10 ccut 25360 . . . . . . . 8  class Cut
119, 10cfv 4592 . . . . . . 7  class  (Cut `  g )
125, 7, 11co 5710 . . . . . 6  class  ( ( 1st `  u ) (Cut `  g )
( 2nd `  u
) )
13 c0 3362 . . . . . 6  class  (/)
1412, 13wne 2412 . . . . 5  wff  ( ( 1st `  u ) (Cut `  g )
( 2nd `  u
) )  =/=  (/)
15 vl . . . . . . 7  set  l
1615cv 1618 . . . . . 6  class  l
17 cslices 25358 . . . . . . 7  class slices
189, 17cfv 4592 . . . . . 6  class  (slices `  g )
1916, 18cfv 4592 . . . . 5  class  ( (slices `  g ) `  l
)
2014, 2, 19wral 2509 . . . 4  wff  A. u  e.  ( (slices `  g
) `  l )
( ( 1st `  u
) (Cut `  g
) ( 2nd `  u
) )  =/=  (/)
21 cplines 25224 . . . . 5  class PLines
229, 21cfv 4592 . . . 4  class  (PLines `  g )
2320, 15, 22wral 2509 . . 3  wff  A. l  e.  (PLines `  g ) A. u  e.  (
(slices `  g ) `  l ) ( ( 1st `  u ) (Cut `  g )
( 2nd `  u
) )  =/=  (/)
24 cibcg 25347 . . 3  class Ibcg
2523, 8, 24crab 2512 . 2  class  { g  e. Ibcg  |  A. l  e.  (PLines `  g ) A. u  e.  (
(slices `  g ) `  l ) ( ( 1st `  u ) (Cut `  g )
( 2nd `  u
) )  =/=  (/) }
261, 25wceq 1619 1  wff Neug  =  {
g  e. Ibcg  |  A. l  e.  (PLines `  g
) A. u  e.  ( (slices `  g
) `  l )
( ( 1st `  u
) (Cut `  g
) ( 2nd `  u
) )  =/=  (/) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator