Definition df-colinear 36726

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 36724	. 2 class Colinear
2		va	. . . . . . . . 9 setvar 𝑎
3	2	cv 1569	. . . . . . . 8 class 𝑎
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1569	. . . . . . . . 9 class 𝑛
6		cee 29399	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6527	. . . . . . . 8 class (𝔼‘𝑛)
8	3, 7	wcel 2145	. . . . . . 7 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . . 9 setvar 𝑏
10	9	cv 1569	. . . . . . . 8 class 𝑏
11	10, 7	wcel 2145	. . . . . . 7 wff 𝑏 ∈ (𝔼‘𝑛)
12		vc	. . . . . . . . 9 setvar 𝑐
13	12	cv 1569	. . . . . . . 8 class 𝑐
14	13, 7	wcel 2145	. . . . . . 7 wff 𝑐 ∈ (𝔼‘𝑛)
15	8, 11, 14	w3a 1103	. . . . . 6 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛))
16	10, 13	cop 4589	. . . . . . . 8 class ⟨𝑏, 𝑐⟩
17		cbtwn 29400	. . . . . . . 8 class Btwn
18	3, 16, 17	wbr 5102	. . . . . . 7 wff 𝑎 Btwn ⟨𝑏, 𝑐⟩
19	13, 3	cop 4589	. . . . . . . 8 class ⟨𝑐, 𝑎⟩
20	10, 19, 17	wbr 5102	. . . . . . 7 wff 𝑏 Btwn ⟨𝑐, 𝑎⟩
21	3, 10	cop 4589	. . . . . . . 8 class ⟨𝑎, 𝑏⟩
22	13, 21, 17	wbr 5102	. . . . . . 7 wff 𝑐 Btwn ⟨𝑎, 𝑏⟩
23	18, 20, 22	w3o 1102	. . . . . 6 wff (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩)
24	15, 23	wa 401	. . . . 5 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
25		cn 12305	. . . . 5 class ℕ
26	24, 4, 25	wrex 3086	. . . 4 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
27	26, 9, 12, 2	coprab 7409	. . 3 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
28	27	ccnv 5646	. 2 class ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
29	1, 28	wceq 1570	1 wff Colinear = ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}

This definition is used by:  colinrel  36744  brcolinear2  36745  colinearex  36747  colineardim1  36748