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

Ref Expression
Assertion df-plig Plig = { 𝑥 ∣ ( ∀ 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝑥𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplig Plig
1 vx 𝑥
2 va 𝑎
3 1 cv 𝑥
4 3 cuni 𝑥
5 vb 𝑏
6 2 cv 𝑎
7 5 cv 𝑏
8 6 7 wne 𝑎𝑏
9 vl 𝑙
10 9 cv 𝑙
11 6 10 wcel 𝑎𝑙
12 7 10 wcel 𝑏𝑙
13 11 12 wa ( 𝑎𝑙𝑏𝑙 )
14 13 9 3 wreu ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 )
15 8 14 wi ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) )
16 15 5 4 wral 𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) )
17 16 2 4 wral 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) )
18 8 11 12 w3a ( 𝑎𝑏𝑎𝑙𝑏𝑙 )
19 18 5 4 wrex 𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 )
20 19 2 4 wrex 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 )
21 20 9 3 wral 𝑙𝑥𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 )
22 vc 𝑐
23 22 cv 𝑐
24 23 10 wcel 𝑐𝑙
25 11 12 24 w3a ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
26 25 wn ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
27 26 9 3 wral 𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
28 27 22 4 wrex 𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
29 28 5 4 wrex 𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
30 29 2 4 wrex 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 )
31 17 21 30 w3a ( ∀ 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝑥𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) )
32 31 1 cab { 𝑥 ∣ ( ∀ 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝑥𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) }
33 0 32 wceq Plig = { 𝑥 ∣ ( ∀ 𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏 → ∃! 𝑙𝑥 ( 𝑎𝑙𝑏𝑙 ) ) ∧ ∀ 𝑙𝑥𝑎 𝑥𝑏 𝑥 ( 𝑎𝑏𝑎𝑙𝑏𝑙 ) ∧ ∃ 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ ( 𝑎𝑙𝑏𝑙𝑐𝑙 ) ) }