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 ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ 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 class Plig
1 vx setvar x
2 va setvar a
3 1 cv setvar x
4 3 cuni class ⋃ x
5 vb setvar b
6 2 cv setvar a
7 5 cv setvar b
8 6 7 wne wff a ≠ b
9 vl setvar l
10 9 cv setvar l
11 6 10 wcel wff a ∈ l
12 7 10 wcel wff b ∈ l
13 11 12 wa wff a ∈ l ∧ b ∈ l
14 13 9 3 wreu wff ∃! l ∈ x a ∈ l ∧ b ∈ l
15 8 14 wi wff a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l
16 15 5 4 wral wff ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l
17 16 2 4 wral wff ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l
18 8 11 12 w3a wff a ≠ b ∧ a ∈ l ∧ b ∈ l
19 18 5 4 wrex wff ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l
20 19 2 4 wrex wff ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l
21 20 9 3 wral wff ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l
22 vc setvar c
23 22 cv setvar c
24 23 10 wcel wff c ∈ l
25 11 12 24 w3a wff a ∈ 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 ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
32 31 1 cab class x | ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l
33 0 32 wceq wff Plig = x | ∀ a ∈ ⋃ x ∀ b ∈ ⋃ x a ≠ b → ∃! l ∈ x a ∈ l ∧ b ∈ l ∧ ∀ l ∈ x ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x a ≠ b ∧ a ∈ l ∧ b ∈ l ∧ ∃ a ∈ ⋃ x ∃ b ∈ ⋃ x ∃ c ∈ ⋃ x ∀ l ∈ x ¬ a ∈ l ∧ b ∈ l ∧ c ∈ l