Metamath Proof Explorer

Theorem brcolinear

Description: The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion brcolinear 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )

Proof

Step Hyp Ref Expression
1 brcolinear2 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Colinear <. B , C >. <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
2 1 3adant1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Colinear <. B , C >. <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
3 2 adantl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
4 simpr 
 |-  ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) -> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )
5 4 rexlimivw 
 |-  ( E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) -> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )
6 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
7 6 eleq2d 
 |-  ( n = N -> ( A e. ( EE ` n ) <-> A e. ( EE ` N ) ) )
8 6 eleq2d 
 |-  ( n = N -> ( B e. ( EE ` n ) <-> B e. ( EE ` N ) ) )
9 6 eleq2d 
 |-  ( n = N -> ( C e. ( EE ` n ) <-> C e. ( EE ` N ) ) )
10 7 8 9 3anbi123d 
 |-  ( n = N -> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) )
11 10 anbi1d 
 |-  ( n = N -> ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) <-> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
12 11 rspcev 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) -> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
13 12 expr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) -> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) ) )
14 5 13 impbid2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ C e. ( EE ` n ) ) /\ ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
15 3 14 bitrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )