Metamath Proof Explorer

Theorem brcolinear2

Description: Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion brcolinear2 
|- ( ( Q e. V /\ R e. W ) -> ( P Colinear <. Q , R >. <-> 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 >. ) ) ) )

Proof

Step Hyp Ref Expression
1 colinrel 
 |-  Rel Colinear
2 1 brrelex1i 
 |-  ( P Colinear <. Q , R >. -> P e. _V )
3 2 a1i 
 |-  ( ( Q e. V /\ R e. W ) -> ( P Colinear <. Q , R >. -> P e. _V ) )
4 elex 
 |-  ( P e. ( EE ` n ) -> P e. _V )
5 4 3ad2ant1 
 |-  ( ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) -> P e. _V )
6 5 adantr 
 |-  ( ( ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) /\ ( P Btwn <. Q , R >. \/ Q Btwn <. R , P >. \/ R Btwn <. P , Q >. ) ) -> P e. _V )
7 6 rexlimivw 
 |-  ( 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 >. ) ) -> P e. _V )
8 7 a1i 
 |-  ( ( Q e. V /\ R e. W ) -> ( 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 >. ) ) -> P e. _V ) )
9 df-br 
 |-  ( P Colinear <. Q , R >. <-> <. P , <. Q , R >. >. e. Colinear )
10 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 >. ) ) }
11 10 eleq2i 
 |-  ( <. P , <. Q , R >. >. e. Colinear <-> <. P , <. Q , R >. >. e. `' { <. <. 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 >. ) ) } )
12 9 11 bitri 
 |-  ( P Colinear <. Q , R >. <-> <. P , <. Q , R >. >. e. `' { <. <. 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 >. ) ) } )
13 opex 
 |-  <. Q , R >. e. _V
14 opelcnvg 
 |-  ( ( P e. _V /\ <. Q , R >. e. _V ) -> ( <. P , <. Q , R >. >. e. `' { <. <. 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 >. ) ) } <-> <. <. Q , R >. , P >. e. { <. <. 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 >. ) ) } ) )
15 13 14 mpan2 
 |-  ( P e. _V -> ( <. P , <. Q , R >. >. e. `' { <. <. 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 >. ) ) } <-> <. <. Q , R >. , P >. e. { <. <. 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 >. ) ) } ) )
16 15 3ad2ant3 
 |-  ( ( Q e. V /\ R e. W /\ P e. _V ) -> ( <. P , <. Q , R >. >. e. `' { <. <. 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 >. ) ) } <-> <. <. Q , R >. , P >. e. { <. <. 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 >. ) ) } ) )
17 12 16 syl5bb 
 |-  ( ( Q e. V /\ R e. W /\ P e. _V ) -> ( P Colinear <. Q , R >. <-> <. <. Q , R >. , P >. e. { <. <. 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 >. ) ) } ) )
18 eleq1 
 |-  ( q = Q -> ( q e. ( EE ` n ) <-> Q e. ( EE ` n ) ) )
19 18 3anbi2d 
 |-  ( q = Q -> ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ r e. ( EE ` n ) ) <-> ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ r e. ( EE ` n ) ) ) )
20 opeq1 
 |-  ( q = Q -> <. q , r >. = <. Q , r >. )
21 20 breq2d 
 |-  ( q = Q -> ( p Btwn <. q , r >. <-> p Btwn <. Q , r >. ) )
22 breq1 
 |-  ( q = Q -> ( q Btwn <. r , p >. <-> Q Btwn <. r , p >. ) )
23 opeq2 
 |-  ( q = Q -> <. p , q >. = <. p , Q >. )
24 23 breq2d 
 |-  ( q = Q -> ( r Btwn <. p , q >. <-> r Btwn <. p , Q >. ) )
25 21 22 24 3orbi123d 
 |-  ( q = Q -> ( ( p Btwn <. q , r >. \/ q Btwn <. r , p >. \/ r Btwn <. p , q >. ) <-> ( p Btwn <. Q , r >. \/ Q Btwn <. r , p >. \/ r Btwn <. p , Q >. ) ) )
26 19 25 anbi12d 
 |-  ( q = Q -> ( ( ( p e. ( EE ` n ) /\ q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. q , r >. \/ q Btwn <. r , p >. \/ r Btwn <. p , q >. ) ) <-> ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. Q , r >. \/ Q Btwn <. r , p >. \/ r Btwn <. p , Q >. ) ) ) )
27 26 rexbidv 
 |-  ( q = Q -> ( 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 >. ) ) <-> 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 >. ) ) ) )
28 eleq1 
 |-  ( r = R -> ( r e. ( EE ` n ) <-> R e. ( EE ` n ) ) )
29 28 3anbi3d 
 |-  ( r = R -> ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ r e. ( EE ` n ) ) <-> ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) ) )
30 opeq2 
 |-  ( r = R -> <. Q , r >. = <. Q , R >. )
31 30 breq2d 
 |-  ( r = R -> ( p Btwn <. Q , r >. <-> p Btwn <. Q , R >. ) )
32 opeq1 
 |-  ( r = R -> <. r , p >. = <. R , p >. )
33 32 breq2d 
 |-  ( r = R -> ( Q Btwn <. r , p >. <-> Q Btwn <. R , p >. ) )
34 breq1 
 |-  ( r = R -> ( r Btwn <. p , Q >. <-> R Btwn <. p , Q >. ) )
35 31 33 34 3orbi123d 
 |-  ( r = R -> ( ( p Btwn <. Q , r >. \/ Q Btwn <. r , p >. \/ r Btwn <. p , Q >. ) <-> ( p Btwn <. Q , R >. \/ Q Btwn <. R , p >. \/ R Btwn <. p , Q >. ) ) )
36 29 35 anbi12d 
 |-  ( r = R -> ( ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ r e. ( EE ` n ) ) /\ ( p Btwn <. Q , r >. \/ Q Btwn <. r , p >. \/ r Btwn <. p , Q >. ) ) <-> ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) /\ ( p Btwn <. Q , R >. \/ Q Btwn <. R , p >. \/ R Btwn <. p , Q >. ) ) ) )
37 36 rexbidv 
 |-  ( r = R -> ( 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 >. ) ) <-> 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 >. ) ) ) )
38 eleq1 
 |-  ( p = P -> ( p e. ( EE ` n ) <-> P e. ( EE ` n ) ) )
39 38 3anbi1d 
 |-  ( p = P -> ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) <-> ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) ) )
40 breq1 
 |-  ( p = P -> ( p Btwn <. Q , R >. <-> P Btwn <. Q , R >. ) )
41 opeq2 
 |-  ( p = P -> <. R , p >. = <. R , P >. )
42 41 breq2d 
 |-  ( p = P -> ( Q Btwn <. R , p >. <-> Q Btwn <. R , P >. ) )
43 opeq1 
 |-  ( p = P -> <. p , Q >. = <. P , Q >. )
44 43 breq2d 
 |-  ( p = P -> ( R Btwn <. p , Q >. <-> R Btwn <. P , Q >. ) )
45 40 42 44 3orbi123d 
 |-  ( p = P -> ( ( p Btwn <. Q , R >. \/ Q Btwn <. R , p >. \/ R Btwn <. p , Q >. ) <-> ( P Btwn <. Q , R >. \/ Q Btwn <. R , P >. \/ R Btwn <. P , Q >. ) ) )
46 39 45 anbi12d 
 |-  ( p = P -> ( ( ( p e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) /\ ( p Btwn <. Q , R >. \/ Q Btwn <. R , p >. \/ R Btwn <. p , Q >. ) ) <-> ( ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ R e. ( EE ` n ) ) /\ ( P Btwn <. Q , R >. \/ Q Btwn <. R , P >. \/ R Btwn <. P , Q >. ) ) ) )
47 46 rexbidv 
 |-  ( p = 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 >. ) ) <-> 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 >. ) ) ) )
48 27 37 47 eloprabg 
 |-  ( ( Q e. V /\ R e. W /\ P e. _V ) -> ( <. <. Q , R >. , P >. e. { <. <. 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 >. ) ) } <-> 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 >. ) ) ) )
49 17 48 bitrd 
 |-  ( ( Q e. V /\ R e. W /\ P e. _V ) -> ( P Colinear <. Q , R >. <-> 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 >. ) ) ) )
50 49 3expia 
 |-  ( ( Q e. V /\ R e. W ) -> ( P e. _V -> ( P Colinear <. Q , R >. <-> 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 >. ) ) ) ) )
51 3 8 50 pm5.21ndd 
 |-  ( ( Q e. V /\ R e. W ) -> ( P Colinear <. Q , R >. <-> 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 >. ) ) ) )