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 Ibcg PLines slicesCut
Distinct variable group:   ,,

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