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	⊢ Rel Colinear

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) }
2		df-colinear	⊢ Colinear = ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) }
3	2	releqi	⊢ ( Rel Colinear ↔ Rel ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } )
4	1 3	mpbir	⊢ Rel Colinear