Metamath Proof Explorer

Theorem colinearex

Description: The colinear predicate exists. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colinearex 
|- Colinear e. _V

Proof

Step Hyp Ref Expression
1 df-colinear 
 |-  Colinear = `' { <. <. b , c >. , a >. | 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 nnex 
 |-  NN e. _V
3 fvex 
 |-  ( EE ` n ) e. _V
4 3 3 xpex 
 |-  ( ( EE ` n ) X. ( EE ` n ) ) e. _V
5 4 3 xpex 
 |-  ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) e. _V
6 2 5 iunex 
 |-  U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) e. _V
7 df-oprab 
 |-  { <. <. b , c >. , a >. | 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 >. ) ) } = { x | E. b E. c E. a ( x = <. <. b , c >. , a >. /\ 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 >. ) ) ) }
8 opelxpi 
 |-  ( ( b e. ( EE ` n ) /\ c e. ( EE ` n ) ) -> <. b , c >. e. ( ( EE ` n ) X. ( EE ` n ) ) )
9 8 3adant1 
 |-  ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) -> <. b , c >. e. ( ( EE ` n ) X. ( EE ` n ) ) )
10 simp1 
 |-  ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) -> a e. ( EE ` n ) )
11 opelxpi 
 |-  ( ( <. b , c >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ a e. ( EE ` n ) ) -> <. <. b , c >. , a >. e. ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
12 9 10 11 syl2anc 
 |-  ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) -> <. <. b , c >. , a >. e. ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
13 12 adantr 
 |-  ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) -> <. <. b , c >. , a >. e. ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
14 13 reximi 
 |-  ( 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 >. ) ) -> E. n e. NN <. <. b , c >. , a >. e. ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
15 eliun 
 |-  ( <. <. b , c >. , a >. e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) <-> E. n e. NN <. <. b , c >. , a >. e. ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
16 14 15 sylibr 
 |-  ( 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 >. ) ) -> <. <. b , c >. , a >. e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
17 eleq1 
 |-  ( x = <. <. b , c >. , a >. -> ( x e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) <-> <. <. b , c >. , a >. e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) ) )
18 17 biimpar 
 |-  ( ( x = <. <. b , c >. , a >. /\ <. <. b , c >. , a >. e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) ) -> x e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
19 16 18 sylan2 
 |-  ( ( x = <. <. b , c >. , a >. /\ 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 >. ) ) ) -> x e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
20 19 exlimiv 
 |-  ( E. a ( x = <. <. b , c >. , a >. /\ 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 >. ) ) ) -> x e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
21 20 exlimivv 
 |-  ( E. b E. c E. a ( x = <. <. b , c >. , a >. /\ 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 >. ) ) ) -> x e. U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) ) )
22 21 abssi 
 |-  { x | E. b E. c E. a ( x = <. <. b , c >. , a >. /\ 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 >. ) ) ) } C_ U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) )
23 7 22 eqsstri 
 |-  { <. <. b , c >. , a >. | 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 >. ) ) } C_ U_ n e. NN ( ( ( EE ` n ) X. ( EE ` n ) ) X. ( EE ` n ) )
24 6 23 ssexi 
 |-  { <. <. b , c >. , a >. | 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 >. ) ) } e. _V
25 24 cnvex 
 |-  `' { <. <. b , c >. , a >. | 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 >. ) ) } e. _V
26 1 25 eqeltri 
 |-  Colinear e. _V