| 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 ) ) |