Metamath Proof Explorer

Definition df-plig

Description: Define the class of planar incidence geometries. We use Hilbert's axioms and adapt them to planar geometry. We use e. for the incidence relation. We could have used a generic binary relation, but using e. allows to reuse previous results. Much of what follows is directly borrowed from Aitken,Incidence-Betweenness Geometry, 2008, http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf .

The class Plig is the class of planar incidence geometries, where a planar incidence geometry is defined as a set of lines satisfying three axioms. In the definition below, x denotes a planar incidence geometry, so U. x denotes the union of its lines, that is, the set of points in the plane, l denotes a line, and a , b , c denote points. Therefore, the axioms are: 1) for all pairs of (distinct) points, there exists a unique line containing them; 2) all lines contain at least two points; 3) there exist three non-collinear points. (Contributed by FL, 2-Aug-2009)

Ref Expression
Assertion df-plig 
|- Plig = { x | ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplig 
 |-  Plig
1 vx 
 |-  x
2 va 
 |-  a
3 1 cv 
 |-  x
4 3 cuni 
 |-  U. x
5 vb 
 |-  b
6 2 cv 
 |-  a
7 5 cv 
 |-  b
8 6 7 wne 
 |-  a =/= b
9 vl 
 |-  l
10 9 cv 
 |-  l
11 6 10 wcel 
 |-  a e. l
12 7 10 wcel 
 |-  b e. l
13 11 12 wa 
 |-  ( a e. l /\ b e. l )
14 13 9 3 wreu 
 |-  E! l e. x ( a e. l /\ b e. l )
15 8 14 wi 
 |-  ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
16 15 5 4 wral 
 |-  A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
17 16 2 4 wral 
 |-  A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
18 8 11 12 w3a 
 |-  ( a =/= b /\ a e. l /\ b e. l )
19 18 5 4 wrex 
 |-  E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
20 19 2 4 wrex 
 |-  E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
21 20 9 3 wral 
 |-  A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
22 vc 
 |-  c
23 22 cv 
 |-  c
24 23 10 wcel 
 |-  c e. l
25 11 12 24 w3a 
 |-  ( a e. l /\ b e. l /\ c e. l )
26 25 wn 
 |-  -. ( a e. l /\ b e. l /\ c e. l )
27 26 9 3 wral 
 |-  A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
28 27 22 4 wrex 
 |-  E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
29 28 5 4 wrex 
 |-  E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
30 29 2 4 wrex 
 |-  E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
31 17 21 30 w3a 
 |-  ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) )
32 31 1 cab 
 |-  { x | ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) ) }
33 0 32 wceq 
 |-  Plig = { x | ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) ) }