Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-colinear Structured version   Visualization version   GIF version

Definition df-colinear 31122
Description: The colinearity predicate states that the three points in its arguments sit on one line. Definition 4.10 of [Schwabhauser] p. 36. (Contributed by Scott Fenton, 25-Oct-2013.)
Assertion
Ref Expression
df-colinear Colinear = {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
Distinct variable group:   𝑎,𝑏,𝑐,𝑛

Detailed syntax breakdown of Definition df-colinear
StepHypRef Expression
1 ccolin 31120 . 2 class Colinear
2 va . . . . . . . . 9 setvar 𝑎
32cv 1473 . . . . . . . 8 class 𝑎
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1473 . . . . . . . . 9 class 𝑛
6 cee 25486 . . . . . . . . 9 class 𝔼
75, 6cfv 5790 . . . . . . . 8 class (𝔼‘𝑛)
83, 7wcel 1976 . . . . . . 7 wff 𝑎 ∈ (𝔼‘𝑛)
9 vb . . . . . . . . 9 setvar 𝑏
109cv 1473 . . . . . . . 8 class 𝑏
1110, 7wcel 1976 . . . . . . 7 wff 𝑏 ∈ (𝔼‘𝑛)
12 vc . . . . . . . . 9 setvar 𝑐
1312cv 1473 . . . . . . . 8 class 𝑐
1413, 7wcel 1976 . . . . . . 7 wff 𝑐 ∈ (𝔼‘𝑛)
158, 11, 14w3a 1030 . . . . . 6 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛))
1610, 13cop 4130 . . . . . . . 8 class 𝑏, 𝑐
17 cbtwn 25487 . . . . . . . 8 class Btwn
183, 16, 17wbr 4577 . . . . . . 7 wff 𝑎 Btwn ⟨𝑏, 𝑐
1913, 3cop 4130 . . . . . . . 8 class 𝑐, 𝑎
2010, 19, 17wbr 4577 . . . . . . 7 wff 𝑏 Btwn ⟨𝑐, 𝑎
213, 10cop 4130 . . . . . . . 8 class 𝑎, 𝑏
2213, 21, 17wbr 4577 . . . . . . 7 wff 𝑐 Btwn ⟨𝑎, 𝑏
2318, 20, 22w3o 1029 . . . . . 6 wff (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩)
2415, 23wa 382 . . . . 5 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
25 cn 10867 . . . . 5 class
2624, 4, 25wrex 2896 . . . 4 wff 𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
2726, 9, 12, 2coprab 6528 . . 3 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
2827ccnv 5027 . 2 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
291, 28wceq 1474 1 wff Colinear = {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
Colors of variables: wff setvar class
This definition is referenced by:  colinrel  31140  brcolinear2  31141  colinearex  31143  colineardim1  31144
  Copyright terms: Public domain W3C validator