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 V

Proof

Step Hyp Ref Expression
1 df-colinear Colinear = b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1
2 nnex V
3 fvex 𝔼 n V
4 3 3 xpex 𝔼 n × 𝔼 n V
5 4 3 xpex 𝔼 n × 𝔼 n × 𝔼 n V
6 2 5 iunex n 𝔼 n × 𝔼 n × 𝔼 n V
7 df-oprab b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b = x | b c a x = b c a n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b
8 opelxpi b 𝔼 n c 𝔼 n b c 𝔼 n × 𝔼 n
9 8 3adant1 a 𝔼 n b 𝔼 n c 𝔼 n b c 𝔼 n × 𝔼 n
10 simp1 a 𝔼 n b 𝔼 n c 𝔼 n a 𝔼 n
11 opelxpi b c 𝔼 n × 𝔼 n a 𝔼 n b c a 𝔼 n × 𝔼 n × 𝔼 n
12 9 10 11 syl2anc a 𝔼 n b 𝔼 n c 𝔼 n b c a 𝔼 n × 𝔼 n × 𝔼 n
13 12 adantr a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b b c a 𝔼 n × 𝔼 n × 𝔼 n
14 13 reximi n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n b c a 𝔼 n × 𝔼 n × 𝔼 n
15 eliun b c a n 𝔼 n × 𝔼 n × 𝔼 n n b c a 𝔼 n × 𝔼 n × 𝔼 n
16 14 15 sylibr n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b b c a n 𝔼 n × 𝔼 n × 𝔼 n
17 eleq1 x = b c a x n 𝔼 n × 𝔼 n × 𝔼 n b c a n 𝔼 n × 𝔼 n × 𝔼 n
18 17 biimpar x = b c a b c a n 𝔼 n × 𝔼 n × 𝔼 n x n 𝔼 n × 𝔼 n × 𝔼 n
19 16 18 sylan2 x = b c a n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b x n 𝔼 n × 𝔼 n × 𝔼 n
20 19 exlimiv a x = b c a n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b x n 𝔼 n × 𝔼 n × 𝔼 n
21 20 exlimivv b c a x = b c a n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b x n 𝔼 n × 𝔼 n × 𝔼 n
22 21 abssi x | b c a x = b c a n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n 𝔼 n × 𝔼 n × 𝔼 n
23 7 22 eqsstri b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b n 𝔼 n × 𝔼 n × 𝔼 n
24 6 23 ssexi b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b V
25 24 cnvex b c a | n a 𝔼 n b 𝔼 n c 𝔼 n a Btwn b c b Btwn c a c Btwn a b -1 V
26 1 25 eqeltri Colinear V