Metamath Proof Explorer

Theorem outsideofcom

Description: Commutitivity 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 >. ) )