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 = ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }
2 nnex ⊢ ℕ ∈ V
3 fvex ⊢ ( 𝔼 ‘ 𝑛 ) ∈ V
4 3 3 xpex ⊢ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∈ V
5 4 3 xpex ⊢ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ∈ V
6 2 5 iunex ⊢ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ∈ V
7 df-oprab ⊢ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } = { 𝑥 ∣ ∃ 𝑏 ∃ 𝑐 ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ) }
8 opelxpi ⊢ ( ( 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) → ⟨ 𝑏 , 𝑐 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) )
9 8 3adant1 ⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) → ⟨ 𝑏 , 𝑐 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) )
10 simp1 ⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) → 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) )
11 opelxpi ⊢ ( ( ⟨ 𝑏 , 𝑐 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ) → ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
12 9 10 11 syl2anc ⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) → ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
13 12 adantr ⊢ ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) → ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
14 13 reximi ⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) → ∃ 𝑛 ∈ ℕ ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
15 eliun ⊢ ( ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕ ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
16 14 15 sylibr ⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) → ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
17 eleq1 ⊢ ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ → ( 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ) )
18 17 biimpar ⊢ ( ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
19 16 18 sylan2 ⊢ ( ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
21 20 exlimivv ⊢ ( ∃ 𝑏 ∃ 𝑐 ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) ) )
22 21 abssi ⊢ { 𝑥 ∣ ∃ 𝑏 ∃ 𝑐 ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∧ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ) } ⊆ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) )
23 7 22 eqsstri ⊢ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ⊆ ∪ 𝑛 ∈ ℕ ( ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) × ( 𝔼 ‘ 𝑛 ) )
24 6 23 ssexi ⊢ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ∈ V
25 24 cnvex ⊢ ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ∈ V
26 1 25 eqeltri ⊢ Colinear ∈ V