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