MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-plig Structured version   Visualization version   GIF version

Definition df-plig 28179
Description: Define the class of planar incidence geometries. We use Hilbert's axioms and adapt them to planar geometry. We use for the incidence relation. We could have used a generic binary relation, but using 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, 𝑥 denotes a planar incidence geometry, so 𝑥 denotes the union of its lines, that is, the set of points in the plane, 𝑙 denotes a line, and 𝑎, 𝑏, 𝑐 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 = {𝑥 ∣ (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))}
Distinct variable group:   𝑥,𝑎,𝑏,𝑐,𝑙

Detailed syntax breakdown of Definition df-plig
StepHypRef Expression
1 cplig 28178 . 2 class Plig
2 va . . . . . . . . 9 setvar 𝑎
32cv 1527 . . . . . . . 8 class 𝑎
4 vb . . . . . . . . 9 setvar 𝑏
54cv 1527 . . . . . . . 8 class 𝑏
63, 5wne 3013 . . . . . . 7 wff 𝑎𝑏
7 vl . . . . . . . . . 10 setvar 𝑙
82, 7wel 2106 . . . . . . . . 9 wff 𝑎𝑙
94, 7wel 2106 . . . . . . . . 9 wff 𝑏𝑙
108, 9wa 396 . . . . . . . 8 wff (𝑎𝑙𝑏𝑙)
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1527 . . . . . . . 8 class 𝑥
1310, 7, 12wreu 3137 . . . . . . 7 wff ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)
146, 13wi 4 . . . . . 6 wff (𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
1512cuni 4830 . . . . . 6 class 𝑥
1614, 4, 15wral 3135 . . . . 5 wff 𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
1716, 2, 15wral 3135 . . . 4 wff 𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
186, 8, 9w3a 1079 . . . . . . 7 wff (𝑎𝑏𝑎𝑙𝑏𝑙)
1918, 4, 15wrex 3136 . . . . . 6 wff 𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
2019, 2, 15wrex 3136 . . . . 5 wff 𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
2120, 7, 12wral 3135 . . . 4 wff 𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
22 vc . . . . . . . . . . 11 setvar 𝑐
2322, 7wel 2106 . . . . . . . . . 10 wff 𝑐𝑙
248, 9, 23w3a 1079 . . . . . . . . 9 wff (𝑎𝑙𝑏𝑙𝑐𝑙)
2524wn 3 . . . . . . . 8 wff ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2625, 7, 12wral 3135 . . . . . . 7 wff 𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2726, 22, 15wrex 3136 . . . . . 6 wff 𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2827, 4, 15wrex 3136 . . . . 5 wff 𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2928, 2, 15wrex 3136 . . . 4 wff 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
3017, 21, 29w3a 1079 . . 3 wff (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))
3130, 11cab 2796 . 2 class {𝑥 ∣ (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))}
321, 31wceq 1528 1 wff Plig = {𝑥 ∣ (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))}
Colors of variables: wff setvar class
This definition is referenced by:  isplig  28180
  Copyright terms: Public domain W3C validator