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=bca|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab-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 ⊢bca|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab=x|∃b∃c∃ax=bca∧∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab
8 opelxpi ⊢b∈𝔼⁡n∧c∈𝔼⁡n→bc∈𝔼⁡n×𝔼⁡n
9 8 3adant1 ⊢a∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n→bc∈𝔼⁡n×𝔼⁡n
10 simp1 ⊢a∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n→a∈𝔼⁡n
11 opelxpi ⊢bc∈𝔼⁡n×𝔼⁡n∧a∈𝔼⁡n→bca∈𝔼⁡n×𝔼⁡n×𝔼⁡n
12 9 10 11 syl2anc ⊢a∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n→bca∈𝔼⁡n×𝔼⁡n×𝔼⁡n
13 12 adantr ⊢a∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→bca∈𝔼⁡n×𝔼⁡n×𝔼⁡n
14 13 reximi ⊢∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→∃n∈ℕbca∈𝔼⁡n×𝔼⁡n×𝔼⁡n
15 eliun ⊢bca∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n↔∃n∈ℕbca∈𝔼⁡n×𝔼⁡n×𝔼⁡n
16 14 15 sylibr ⊢∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→bca∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
17 eleq1 ⊢x=bca→x∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n↔bca∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
18 17 biimpar ⊢x=bca∧bca∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n→x∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
19 16 18 sylan2 ⊢x=bca∧∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→x∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
20 19 exlimiv ⊢∃ax=bca∧∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→x∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
21 20 exlimivv ⊢∃b∃c∃ax=bca∧∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab→x∈⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
22 21 abssi ⊢x|∃b∃c∃ax=bca∧∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab⊆⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
23 7 22 eqsstri ⊢bca|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab⊆⋃n∈ℕ𝔼⁡n×𝔼⁡n×𝔼⁡n
24 6 23 ssexi ⊢bca|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab∈V
25 24 cnvex ⊢bca|∃n∈ℕa∈𝔼⁡n∧b∈𝔼⁡n∧c∈𝔼⁡n∧aBtwnbc∨bBtwnca∨cBtwnab-1∈V
26 1 25 eqeltri ⊢Colinear∈V