Metamath Proof Explorer

Theorem sotrieq2

Description: Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999)

		Ref	Expression
	Assertion	sotrieq2	\|- ( ( 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		ioran	\|- ( -. ( B R C \/ C R B ) <-> ( -. B R C /\ -. C R B ) )
3	1 2	bitrdi	\|- ( ( 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 ) ) )

 |-  ( -. ( B R C \/ C R B ) <-> ( -. B R C /\ -. C R B ) )

1 2

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