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 = { 𝑥 ∣ ( ∀ 𝑎 ∈ ∪ 𝑥 ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝑥 ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) } |
| 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 = { 𝑥 ∣ ( ∀ 𝑎 ∈ ∪ 𝑥 ∀ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 → ∃! 𝑙 ∈ 𝑥 ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ) ∧ ∀ 𝑙 ∈ 𝑥 ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ) ∧ ∃ 𝑎 ∈ ∪ 𝑥 ∃ 𝑏 ∈ ∪ 𝑥 ∃ 𝑐 ∈ ∪ 𝑥 ∀ 𝑙 ∈ 𝑥 ¬ ( 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ) ) } |