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⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor 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 \in 𝔼 (n)$
11	1	cv	$setvar b$
12	11 9	wcel	$wff b \in 𝔼 (n)$
13	2	cv	$setvar c$
14	13 9	wcel	$wff c \in 𝔼 (n)$
15	10 12 14	w3a	$wff (a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (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⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩)$
24	15 23	wa	$wff ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩))$
25	24 4 5	wrex	$wff \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩))$
26	25 1 2 3	coprab	$class \{⟨⟨b, c⟩, a⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩))\}$
27	26	ccnv	$class {\{⟨⟨b, c⟩, a⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩))\}}^{-1}$
28	0 27	wceq	$wff Colinear = {\{⟨⟨b, c⟩, a⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land c \in 𝔼 (n)) \land (a Btwn ⟨b, c⟩ \lor b Btwn ⟨c, a⟩ \lor c Btwn ⟨a, b⟩))\}}^{-1}$

Metamath Proof Explorer

Definition df-colinear

Detailed syntax breakdown