Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-plig Structured version   Unicode version

Definition df-plig 25753
 Description: Planar incidence geometry. I use Hilbert's "axioms" adapted to planar geometry. is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf (Contributed by FL, 2-Aug-2009.)
Assertion
Ref Expression
df-plig
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-plig
StepHypRef Expression
1 cplig 25752 . 2
2 va . . . . . . . . 9
32cv 1436 . . . . . . . 8
4 vb . . . . . . . . 9
54cv 1436 . . . . . . . 8
63, 5wne 2625 . . . . . . 7
7 vl . . . . . . . . . 10
82, 7wel 1871 . . . . . . . . 9
94, 7wel 1871 . . . . . . . . 9
108, 9wa 370 . . . . . . . 8
11 vx . . . . . . . . 9
1211cv 1436 . . . . . . . 8
1310, 7, 12wreu 2784 . . . . . . 7
146, 13wi 4 . . . . . 6
1512cuni 4222 . . . . . 6
1614, 4, 15wral 2782 . . . . 5
1716, 2, 15wral 2782 . . . 4
186, 8, 9w3a 982 . . . . . . 7
1918, 4, 15wrex 2783 . . . . . 6
2019, 2, 15wrex 2783 . . . . 5
2120, 7, 12wral 2782 . . . 4
22 vc . . . . . . . . . . 11
2322, 7wel 1871 . . . . . . . . . 10
248, 9, 23w3a 982 . . . . . . . . 9
2524wn 3 . . . . . . . 8
2625, 7, 12wral 2782 . . . . . . 7
2726, 22, 15wrex 2783 . . . . . 6
2827, 4, 15wrex 2783 . . . . 5
2928, 2, 15wrex 2783 . . . 4
3017, 21, 29w3a 982 . . 3
3130, 11cab 2414 . 2
321, 31wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  isplig  25754
 Copyright terms: Public domain W3C validator