Metamath Proof Explorer

Theorem sotrine

Description: Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021)

		Ref	Expression
	Assertion	sotrine	\|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B =/= C <-> ( B R C \/ C R B ) ) )

Step	Hyp	Ref	Expression
1		sotrieq	\|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )
2	1	bicomd	\|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. ( B R C \/ C R B ) <-> B = C ) )
3	2	necon1abid	\|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B =/= C <-> ( B R C \/ C R B ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )

 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. ( B R C \/ C R B ) <-> B = C ) )

 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B =/= C <-> ( B R C \/ C R B ) ) )