Definition df-colinear 35011

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 35009	. 2 class Colinear
2		va	. . . . . . . . 9 setvar 𝑎
3	2	cv 1541	. . . . . . . 8 class 𝑎
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1541	. . . . . . . . 9 class 𝑛
6		cee 28146	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6544	. . . . . . . 8 class (𝔼‘𝑛)
8	3, 7	wcel 2107	. . . . . . 7 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . . 9 setvar 𝑏
10	9	cv 1541	. . . . . . . 8 class 𝑏
11	10, 7	wcel 2107	. . . . . . 7 wff 𝑏 ∈ (𝔼‘𝑛)
12		vc	. . . . . . . . 9 setvar 𝑐
13	12	cv 1541	. . . . . . . 8 class 𝑐
14	13, 7	wcel 2107	. . . . . . 7 wff 𝑐 ∈ (𝔼‘𝑛)
15	8, 11, 14	w3a 1088	. . . . . 6 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛))
16	10, 13	cop 4635	. . . . . . . 8 class ⟨𝑏, 𝑐⟩
17		cbtwn 28147	. . . . . . . 8 class Btwn
18	3, 16, 17	wbr 5149	. . . . . . 7 wff 𝑎 Btwn ⟨𝑏, 𝑐⟩
19	13, 3	cop 4635	. . . . . . . 8 class ⟨𝑐, 𝑎⟩
20	10, 19, 17	wbr 5149	. . . . . . 7 wff 𝑏 Btwn ⟨𝑐, 𝑎⟩
21	3, 10	cop 4635	. . . . . . . 8 class ⟨𝑎, 𝑏⟩
22	13, 21, 17	wbr 5149	. . . . . . 7 wff 𝑐 Btwn ⟨𝑎, 𝑏⟩
23	18, 20, 22	w3o 1087	. . . . . 6 wff (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩)
24	15, 23	wa 397	. . . . 5 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
25		cn 12212	. . . . 5 class ℕ
26	24, 4, 25	wrex 3071	. . . 4 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))
27	26, 9, 12, 2	coprab 7410	. . 3 class {⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
28	27	ccnv 5676	. 2 class ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}
29	1, 28	wceq 1542	1 wff Colinear = ◡{⟨⟨𝑏, 𝑐⟩, 𝑎⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn ⟨𝑏, 𝑐⟩ ∨ 𝑏 Btwn ⟨𝑐, 𝑎⟩ ∨ 𝑐 Btwn ⟨𝑎, 𝑏⟩))}

This definition is referenced by:  colinrel  35029  brcolinear2  35030  colinearex  35032  colineardim1  35033