Metamath Proof Explorer

Theorem outsideofrflx

Description: Reflexivity of outsideness. Theorem 6.5 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofrflx ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A ≠ P → P OutsideOf A A

Proof

Step Hyp Ref Expression
1 axbtwnid ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → P Btwn A A → P = A
2 eqcom ⊢ P = A ↔ A = P
3 1 2 imbitrdi ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → P Btwn A A → A = P
4 3 necon3ad ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A ≠ P → ¬ P Btwn A A
5 colineartriv2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → P Colinear A A
6 4 5 jctild ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A ≠ P → P Colinear A A ∧ ¬ P Btwn A A
7 broutsideof ⊢ P OutsideOf A A ↔ P Colinear A A ∧ ¬ P Btwn A A
8 6 7 imbitrrdi ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A ≠ P → P OutsideOf A A