Definition df-plig 27327

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 us 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.)

Assertion

Ref	Expression
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 ) ) }

Distinct variable group:   x, a, b, c, l

Detailed syntax breakdown of Definition df-plig

Step	Hyp	Ref	Expression
1		cplig 27326	. 2 class Plig
2		va	. . . . . . . . 9 setvar a
3	2	cv 1482	. . . . . . . 8 class a
4		vb	. . . . . . . . 9 setvar b
5	4	cv 1482	. . . . . . . 8 class b
6	3, 5	wne 2794	. . . . . . 7 wff a =/= b
7		vl	. . . . . . . . . 10 setvar l
8	2, 7	wel 1991	. . . . . . . . 9 wff a e. l
9	4, 7	wel 1991	. . . . . . . . 9 wff b e. l
10	8, 9	wa 384	. . . . . . . 8 wff ( a e. l /\ b e. l )
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1482	. . . . . . . 8 class x
13	10, 7, 12	wreu 2914	. . . . . . 7 wff E! l e. x ( a e. l /\ b e. l )
14	6, 13	wi 4	. . . . . 6 wff ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
15	12	cuni 4436	. . . . . 6 class U. x
16	14, 4, 15	wral 2912	. . . . 5 wff A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
17	16, 2, 15	wral 2912	. . . 4 wff A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) )
18	6, 8, 9	w3a 1037	. . . . . . 7 wff ( a =/= b /\ a e. l /\ b e. l )
19	18, 4, 15	wrex 2913	. . . . . 6 wff E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
20	19, 2, 15	wrex 2913	. . . . 5 wff E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
21	20, 7, 12	wral 2912	. . . 4 wff A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l )
22		vc	. . . . . . . . . . 11 setvar c
23	22, 7	wel 1991	. . . . . . . . . 10 wff c e. l
24	8, 9, 23	w3a 1037	. . . . . . . . 9 wff ( a e. l /\ b e. l /\ c e. l )
25	24	wn 3	. . . . . . . 8 wff -. ( a e. l /\ b e. l /\ c e. l )
26	25, 7, 12	wral 2912	. . . . . . 7 wff A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
27	26, 22, 15	wrex 2913	. . . . . 6 wff E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
28	27, 4, 15	wrex 2913	. . . . 5 wff E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l )
29	28, 2, 15	wrex 2913	. . . 4 wff 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 )
30	17, 21, 29	w3a 1037	. . 3 wff ( 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 ) )
31	30, 11	cab 2608	. 2 class { 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 ) ) }
32	1, 31	wceq 1483	1 wff 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 ) ) }

This definition is referenced by:  isplig  27328