Metamath Proof Explorer

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 = b c a | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccolin class Colinear
1 vb setvar b
2 vc setvar c
3 va setvar a
4 vn setvar n
5 cn class ℕ
6 3 cv setvar a
7 cee class 𝔼
8 4 cv setvar n
9 8 7 cfv class 𝔼 ⁡ n
10 6 9 wcel wff a ∈ 𝔼 ⁡ n
11 1 cv setvar b
12 11 9 wcel wff b ∈ 𝔼 ⁡ n
13 2 cv setvar c
14 13 9 wcel wff c ∈ 𝔼 ⁡ n
15 10 12 14 w3a wff a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n
16 cbtwn class Btwn
17 11 13 cop class b c
18 6 17 16 wbr wff a Btwn b c
19 13 6 cop class c a
20 11 19 16 wbr wff b Btwn c a
21 6 11 cop class a b
22 13 21 16 wbr wff c Btwn a b
23 18 20 22 w3o wff a Btwn b c ∨ b Btwn c a ∨ c Btwn a b
24 15 23 wa wff a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b
25 24 4 5 wrex wff ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b
26 25 1 2 3 coprab class b c a | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b
27 26 ccnv class b c a | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b -1
28 0 27 wceq wff Colinear = b c a | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ c ∈ 𝔼 ⁡ n ∧ a Btwn b c ∨ b Btwn c a ∨ c Btwn a b -1