Theorem colinrel

Description: Colinearity is a relationship. (Contributed by Scott Fenton, 7-Nov-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	colinrel	$$⊢\mathrm{Rel}\mathrm{Colinear}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left\{⟨⟨q,r⟩,p⟩|\exists n\in \mathbb{N}\left(\left(p\in 𝔼\left(n\right)\wedge q\in 𝔼\left(n\right)\wedge r\in 𝔼\left(n\right)\right)\wedge \left(p\mathrm{Btwn}⟨q,r⟩\vee q\mathrm{Btwn}⟨r,p⟩\vee r\mathrm{Btwn}⟨p,q⟩\right)\right)\right\}}^{-1}$$
2		df-colinear	$$⊢\mathrm{Colinear}={\left\{⟨⟨q,r⟩,p⟩|\exists n\in \mathbb{N}\left(\left(p\in 𝔼\left(n\right)\wedge q\in 𝔼\left(n\right)\wedge r\in 𝔼\left(n\right)\right)\wedge \left(p\mathrm{Btwn}⟨q,r⟩\vee q\mathrm{Btwn}⟨r,p⟩\vee r\mathrm{Btwn}⟨p,q⟩\right)\right)\right\}}^{-1}$$
3	2	releqi	$$⊢\mathrm{Rel}\mathrm{Colinear}\leftrightarrow \mathrm{Rel}{\left\{⟨⟨q,r⟩,p⟩|\exists n\in \mathbb{N}\left(\left(p\in 𝔼\left(n\right)\wedge q\in 𝔼\left(n\right)\wedge r\in 𝔼\left(n\right)\right)\wedge \left(p\mathrm{Btwn}⟨q,r⟩\vee q\mathrm{Btwn}⟨r,p⟩\vee r\mathrm{Btwn}⟨p,q⟩\right)\right)\right\}}^{-1}$$
4	1 3	mpbir	$$⊢\mathrm{Rel}\mathrm{Colinear}$$