Metamath Proof Explorer


Theorem outsideofrflx

Description: Reflexitivity 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 syl6ib 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 syl6ibr N P 𝔼 N A 𝔼 N A P P OutsideOf A A