Metamath Proof Explorer

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 `' { <. <. q , r >. , p >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. q , r >. \/ q Btwn <. r , p >. \/ r Btwn <. p , q >. ) ) }
2 df-colinear 
 |-  Colinear = `' { <. <. q , r >. , p >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. q , r >. \/ q Btwn <. r , p >. \/ r Btwn <. p , q >. ) ) }
3 2 releqi 
 |-  ( Rel Colinear <-> Rel `' { <. <. q , r >. , p >. | E. n e. NN ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. q , r >. \/ q Btwn <. r , p >. \/ r Btwn <. p , q >. ) ) } )
4 1 3 mpbir 
 |-  Rel Colinear