Metamath Proof Explorer


Theorem outsideofcom

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

Ref Expression
Assertion outsideofcom
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> P OutsideOf <. B , A >. ) )

Proof

Step Hyp Ref Expression
1 3ancoma
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( B =/= P /\ A =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
2 orcom
 |-  ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) <-> ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) )
3 2 3anbi3i
 |-  ( ( B =/= P /\ A =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( B =/= P /\ A =/= P /\ ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) ) )
4 1 3 bitri
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( B =/= P /\ A =/= P /\ ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) ) )
5 4 a1i
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( B =/= P /\ A =/= P /\ ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) ) ) )
6 broutsideof2
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
7 3ancomb
 |-  ( ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( P e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
8 broutsideof2
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( P OutsideOf <. B , A >. <-> ( B =/= P /\ A =/= P /\ ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) ) ) )
9 7 8 sylan2b
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. B , A >. <-> ( B =/= P /\ A =/= P /\ ( B Btwn <. P , A >. \/ A Btwn <. P , B >. ) ) ) )
10 5 6 9 3bitr4d
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> P OutsideOf <. B , A >. ) )