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∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l∧∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplig classPlig
1 vx setvarx
2 va setvara
3 1 cv setvarx
4 3 cuni class⋃x
5 vb setvarb
6 2 cv setvara
7 5 cv setvarb
8 6 7 wne wffa≠b
9 vl setvarl
10 9 cv setvarl
11 6 10 wcel wffa∈l
12 7 10 wcel wffb∈l
13 11 12 wa wffa∈l∧b∈l
14 13 9 3 wreu wff∃!l∈xa∈l∧b∈l
15 8 14 wi wffa≠b→∃!l∈xa∈l∧b∈l
16 15 5 4 wral wff∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l
17 16 2 4 wral wff∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l
18 8 11 12 w3a wffa≠b∧a∈l∧b∈l
19 18 5 4 wrex wff∃b∈⋃xa≠b∧a∈l∧b∈l
20 19 2 4 wrex wff∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l
21 20 9 3 wral wff∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l
22 vc setvarc
23 22 cv setvarc
24 23 10 wcel wffc∈l
25 11 12 24 w3a wffa∈l∧b∈l∧c∈l
26 25 wn wff¬a∈l∧b∈l∧c∈l
27 26 9 3 wral wff∀l∈x¬a∈l∧b∈l∧c∈l
28 27 22 4 wrex wff∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l
29 28 5 4 wrex wff∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l
30 29 2 4 wrex wff∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l
31 17 21 30 w3a wff∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l∧∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l
32 31 1 cab classx|∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l∧∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l
33 0 32 wceq wffPlig=x|∀a∈⋃x∀b∈⋃xa≠b→∃!l∈xa∈l∧b∈l∧∀l∈x∃a∈⋃x∃b∈⋃xa≠b∧a∈l∧b∈l∧∃a∈⋃x∃b∈⋃x∃c∈⋃x∀l∈x¬a∈l∧b∈l∧c∈l