Theorem caovord3

Description: Ordering law. (Contributed by NM, 29-Feb-1996)

	Ref	Expression
Hypotheses	caovord.1	|- A e. _V
	caovord.2	|- B e. _V
	caovord.3	|- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
	caovord2.3	|- C e. _V
	caovord2.com	|- ( x F y ) = ( y F x )
	caovord3.4	|- D e. _V
Assertion	caovord3	|- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( A R C <-> D R B ) )

Proof

Step	Hyp	Ref	Expression
1		caovord.1	|- A e. _V
2		caovord.2	|- B e. _V
3		caovord.3	|- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
4		caovord2.3	|- C e. _V
5		caovord2.com	|- ( x F y ) = ( y F x )
6		caovord3.4	|- D e. _V
7	1 4 3 2 5	caovord2	|- ( B e. S -> ( A R C <-> ( A F B ) R ( C F B ) ) )
8	7	adantr	|- ( ( B e. S /\ C e. S ) -> ( A R C <-> ( A F B ) R ( C F B ) ) )
9		breq1	|- ( ( A F B ) = ( C F D ) -> ( ( A F B ) R ( C F B ) <-> ( C F D ) R ( C F B ) ) )
10	8 9	sylan9bb	|- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( A R C <-> ( C F D ) R ( C F B ) ) )
11	6 2 3	caovord	|- ( C e. S -> ( D R B <-> ( C F D ) R ( C F B ) ) )
12	11	ad2antlr	|- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( D R B <-> ( C F D ) R ( C F B ) ) )
13	10 12	bitr4d	|- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( A R C <-> D R B ) )