# 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 ${⊢}\mathrm{Plig}=\left\{{x}|\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cplig ${class}\mathrm{Plig}$
1 vx ${setvar}{x}$
2 va ${setvar}{a}$
3 1 cv ${setvar}{x}$
4 3 cuni ${class}\bigcup {x}$
5 vb ${setvar}{b}$
6 2 cv ${setvar}{a}$
7 5 cv ${setvar}{b}$
8 6 7 wne ${wff}{a}\ne {b}$
9 vl ${setvar}{l}$
10 9 cv ${setvar}{l}$
11 6 10 wcel ${wff}{a}\in {l}$
12 7 10 wcel ${wff}{b}\in {l}$
13 11 12 wa ${wff}\left({a}\in {l}\wedge {b}\in {l}\right)$
14 13 9 3 wreu ${wff}\exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)$
15 8 14 wi ${wff}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)$
16 15 5 4 wral ${wff}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)$
17 16 2 4 wral ${wff}\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)$
18 8 11 12 w3a ${wff}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)$
19 18 5 4 wrex ${wff}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)$
20 19 2 4 wrex ${wff}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)$
21 20 9 3 wral ${wff}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)$
22 vc ${setvar}{c}$
23 22 cv ${setvar}{c}$
24 23 10 wcel ${wff}{c}\in {l}$
25 11 12 24 w3a ${wff}\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
26 25 wn ${wff}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
27 26 9 3 wral ${wff}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
28 27 22 4 wrex ${wff}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
29 28 5 4 wrex ${wff}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
30 29 2 4 wrex ${wff}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)$
31 17 21 30 w3a ${wff}\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)$
32 31 1 cab ${class}\left\{{x}|\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right\}$
33 0 32 wceq ${wff}\mathrm{Plig}=\left\{{x}|\left(\forall {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\to \exists !{l}\in {x}\phantom{\rule{.4em}{0ex}}\left({a}\in {l}\wedge {b}\in {l}\right)\right)\wedge \forall {l}\in {x}\phantom{\rule{.4em}{0ex}}\exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\left({a}\ne {b}\wedge {a}\in {l}\wedge {b}\in {l}\right)\wedge \exists {a}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\exists {c}\in \bigcup {x}\phantom{\rule{.4em}{0ex}}\forall {l}\in {x}\phantom{\rule{.4em}{0ex}}¬\left({a}\in {l}\wedge {b}\in {l}\wedge {c}\in {l}\right)\right)\right\}$