Definition df-colinear

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)

	Ref	Expression
Assertion	df-colinear	⊢ Colinear = ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccolin	⊢ Colinear
1		vb	⊢ 𝑏
2		vc	⊢ 𝑐
3		va	⊢ 𝑎
4		vn	⊢ 𝑛
5		cn	⊢ ℕ
6	3	cv	⊢ 𝑎
7		cee	⊢ 𝔼
8	4	cv	⊢ 𝑛
9	8 7	cfv	⊢ ( 𝔼 ‘ 𝑛 )
10	6 9	wcel	⊢ 𝑎 ∈ ( 𝔼 ‘ 𝑛 )
11	1	cv	⊢ 𝑏
12	11 9	wcel	⊢ 𝑏 ∈ ( 𝔼 ‘ 𝑛 )
13	2	cv	⊢ 𝑐
14	13 9	wcel	⊢ 𝑐 ∈ ( 𝔼 ‘ 𝑛 )
15	10 12 14	w3a	⊢ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) )
16		cbtwn	⊢ Btwn
17	11 13	cop	⊢ ⟨ 𝑏 , 𝑐 ⟩
18	6 17 16	wbr	⊢ 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩
19	13 6	cop	⊢ ⟨ 𝑐 , 𝑎 ⟩
20	11 19 16	wbr	⊢ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩
21	6 11	cop	⊢ ⟨ 𝑎 , 𝑏 ⟩
22	13 21 16	wbr	⊢ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩
23	18 20 22	w3o	⊢ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ )
24	15 23	wa	⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) )
25	24 4 5	wrex	⊢ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) )
26	25 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }
27	26	ccnv	⊢ ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }
28	0 27	wceq	⊢ Colinear = ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }