Metamath Proof Explorer

Theorem caovord3

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

Ref Expression
Hypotheses caovord.1 ⊢A∈V
caovord.2 ⊢B∈V
caovord.3 ⊢z∈S→xRy↔zFxRzFy
caovord2.3 ⊢C∈V
caovord2.com ⊢xFy=yFx
caovord3.4 ⊢D∈V
Assertion caovord3 ⊢B∈S∧C∈S∧AFB=CFD→ARC↔DRB

Proof

Step Hyp Ref Expression
1 caovord.1 ⊢A∈V
2 caovord.2 ⊢B∈V
3 caovord.3 ⊢z∈S→xRy↔zFxRzFy
4 caovord2.3 ⊢C∈V
5 caovord2.com ⊢xFy=yFx
6 caovord3.4 ⊢D∈V
7 1 4 3 2 5 caovord2 ⊢B∈S→ARC↔AFBRCFB
8 7 adantr ⊢B∈S∧C∈S→ARC↔AFBRCFB
9 breq1 ⊢AFB=CFD→AFBRCFB↔CFDRCFB
10 8 9 sylan9bb ⊢B∈S∧C∈S∧AFB=CFD→ARC↔CFDRCFB
11 6 2 3 caovord ⊢C∈S→DRB↔CFDRCFB
12 11 ad2antlr ⊢B∈S∧C∈S∧AFB=CFD→DRB↔CFDRCFB
13 10 12 bitr4d ⊢B∈S∧C∈S∧AFB=CFD→ARC↔DRB