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 32271
 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 32269 . 2 class Colinear
2 va . . . . . . . . 9 setvar 𝑎
32cv 1522 . . . . . . . 8 class 𝑎
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1522 . . . . . . . . 9 class 𝑛
6 cee 25813 . . . . . . . . 9 class 𝔼
75, 6cfv 5926 . . . . . . . 8 class (𝔼‘𝑛)
83, 7wcel 2030 . . . . . . 7 wff 𝑎 ∈ (𝔼‘𝑛)
9 vb . . . . . . . . 9 setvar 𝑏
109cv 1522 . . . . . . . 8 class 𝑏
1110, 7wcel 2030 . . . . . . 7 wff 𝑏 ∈ (𝔼‘𝑛)
12 vc . . . . . . . . 9 setvar 𝑐
1312cv 1522 . . . . . . . 8 class 𝑐
1413, 7wcel 2030 . . . . . . 7 wff 𝑐 ∈ (𝔼‘𝑛)
158, 11, 14w3a 1054 . . . . . 6 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛))
1610, 13cop 4216 . . . . . . . 8 class 𝑏, 𝑐
17 cbtwn 25814 . . . . . . . 8 class Btwn
183, 16, 17wbr 4685 . . . . . . 7 wff 𝑎 Btwn ⟨𝑏, 𝑐
1913, 3cop 4216 . . . . . . . 8 class 𝑐, 𝑎
2010, 19, 17wbr 4685 . . . . . . 7 wff 𝑏 Btwn ⟨𝑐, 𝑎
213, 10cop 4216 . . . . . . . 8 class 𝑎, 𝑏
2213, 21, 17wbr 4685 . . . . . . 7 wff 𝑐 Btwn ⟨𝑎, 𝑏
2318, 20, 22w3o 1053 . . . . . 6 wff (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩)
2415, 23wa 383 . . . . 5 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
25 cn 11058 . . . . 5 class
2624, 4, 25wrex 2942 . . . 4 wff 𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
2726, 9, 12, 2coprab 6691 . . 3 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
2827ccnv 5142 . 2 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
291, 28wceq 1523 1 wff Colinear = {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
 Colors of variables: wff setvar class This definition is referenced by:  colinrel  32289  brcolinear2  32290  colinearex  32292  colineardim1  32293
 Copyright terms: Public domain W3C validator