Metamath Proof Explorer

Theorem brcolinear

Description: The binary relation form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B

Proof

Step Hyp Ref Expression
1 brcolinear2 ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
2 1 3adant1 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
3 2 adantl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
4 simpr ⊢ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
5 4 rexlimivw ⊢ ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
6 fveq2 ⊢ n = N → 𝔼 ⁡ n = 𝔼 ⁡ N
7 6 eleq2d ⊢ n = N → A ∈ 𝔼 ⁡ n ↔ A ∈ 𝔼 ⁡ N
8 6 eleq2d ⊢ n = N → B ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ N
9 6 eleq2d ⊢ n = N → C ∈ 𝔼 ⁡ n ↔ C ∈ 𝔼 ⁡ N
10 7 8 9 3anbi123d ⊢ n = N → A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ↔ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
11 10 anbi1d ⊢ n = N → A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
12 11 rspcev ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B → ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
13 12 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B → ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
14 5 13 impbid2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ n ∈ ℕ A ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
15 3 14 bitrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B