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

Definition df-plig 26719
 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, ∪ 𝑥 is the union of lines, that is, the plane, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: for all pairs of (distinct) points, there exists a unique line containing them; all lines contain at least two points; 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 26718 . 2 class Plig
2 va . . . . . . . . 9 setvar 𝑎
32cv 1474 . . . . . . . 8 class 𝑎
4 vb . . . . . . . . 9 setvar 𝑏
54cv 1474 . . . . . . . 8 class 𝑏
63, 5wne 2780 . . . . . . 7 wff 𝑎𝑏
7 vl . . . . . . . . . 10 setvar 𝑙
82, 7wel 1978 . . . . . . . . 9 wff 𝑎𝑙
94, 7wel 1978 . . . . . . . . 9 wff 𝑏𝑙
108, 9wa 383 . . . . . . . 8 wff (𝑎𝑙𝑏𝑙)
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1474 . . . . . . . 8 class 𝑥
1310, 7, 12wreu 2898 . . . . . . 7 wff ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)
146, 13wi 4 . . . . . 6 wff (𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
1512cuni 4372 . . . . . 6 class 𝑥
1614, 4, 15wral 2896 . . . . 5 wff 𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
1716, 2, 15wral 2896 . . . 4 wff 𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙))
186, 8, 9w3a 1031 . . . . . . 7 wff (𝑎𝑏𝑎𝑙𝑏𝑙)
1918, 4, 15wrex 2897 . . . . . 6 wff 𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
2019, 2, 15wrex 2897 . . . . 5 wff 𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
2120, 7, 12wral 2896 . . . 4 wff 𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙)
22 vc . . . . . . . . . . 11 setvar 𝑐
2322, 7wel 1978 . . . . . . . . . 10 wff 𝑐𝑙
248, 9, 23w3a 1031 . . . . . . . . 9 wff (𝑎𝑙𝑏𝑙𝑐𝑙)
2524wn 3 . . . . . . . 8 wff ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2625, 7, 12wral 2896 . . . . . . 7 wff 𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2726, 22, 15wrex 2897 . . . . . 6 wff 𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2827, 4, 15wrex 2897 . . . . 5 wff 𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
2928, 2, 15wrex 2897 . . . 4 wff 𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙)
3017, 21, 29w3a 1031 . . 3 wff (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))
3130, 11cab 2596 . 2 class {𝑥 ∣ (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))}
321, 31wceq 1475 1 wff Plig = {𝑥 ∣ (∀𝑎 𝑥𝑏 𝑥(𝑎𝑏 → ∃!𝑙𝑥 (𝑎𝑙𝑏𝑙)) ∧ ∀𝑙𝑥𝑎 𝑥𝑏 𝑥(𝑎𝑏𝑎𝑙𝑏𝑙) ∧ ∃𝑎 𝑥𝑏 𝑥𝑐 𝑥𝑙𝑥 ¬ (𝑎𝑙𝑏𝑙𝑐𝑙))}
 Colors of variables: wff setvar class This definition is referenced by:  isplig  26720
 Copyright terms: Public domain W3C validator