Definition df-colinear 35315

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

Step	Hyp	Ref	Expression
1		ccolin 35313	. 2 class Colinear
2		va	. . . . . . . . 9 setvar 𝑎
3	2	cv 1538	. . . . . . . 8 class 𝑎
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1538	. . . . . . . . 9 class 𝑛
6		cee 28413	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6542	. . . . . . . 8 class (𝔼‘𝑛)
8	3, 7	wcel 2104	. . . . . . 7 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . . 9 setvar 𝑏
10	9	cv 1538	. . . . . . . 8 class 𝑏
11	10, 7	wcel 2104	. . . . . . 7 wff 𝑏 ∈ (𝔼‘𝑛)
12		vc	. . . . . . . . 9 setvar 𝑐
13	12	cv 1538	. . . . . . . 8 class 𝑐
14	13, 7	wcel 2104	. . . . . . 7 wff 𝑐 ∈ (𝔼‘𝑛)
15	8, 11, 14	w3a 1085	. . . . . 6 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛))
16	10, 13	cop 4633	. . . . . . . 8 class ⟨𝑏, 𝑐⟩
17		cbtwn 28414	. . . . . . . 8 class Btwn
18	3, 16, 17	wbr 5147	. . . . . . 7 wff 𝑎 Btwn ⟨𝑏, 𝑐⟩
19	13, 3	cop 4633	. . . . . . . 8 class ⟨𝑐, 𝑎⟩
20	10, 19, 17	wbr 5147	. . . . . . 7 wff 𝑏 Btwn ⟨𝑐, 𝑎⟩
21	3, 10	cop 4633	. . . . . . . 8 class ⟨𝑎, 𝑏⟩
22	13, 21, 17	wbr 5147	. . . . . . 7 wff 𝑐 Btwn ⟨𝑎, 𝑏⟩
23	18, 20, 22	w3o 1084	. . . . . 6 wff (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩)
24	15, 23	wa 394	. . . . 5 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
25		cn 12216	. . . . 5 class ℕ
26	24, 4, 25	wrex 3068	. . . 4 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
27	26, 9, 12, 2	coprab 7412	. . 3 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
28	27	ccnv 5674	. 2 class ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
29	1, 28	wceq 1539	1 wff Colinear = ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}

This definition is referenced by:  colinrel  35333  brcolinear2  35334  colinearex  35336  colineardim1  35337