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 → x R y ↔ z F x R z F y
caovord2.3 ⊢ C ∈ V
caovord2.com ⊢ x F y = y F x
caovord3.4 ⊢ D ∈ V
Assertion caovord3 ⊢ B ∈ S ∧ C ∈ S ∧ A F B = C F D → A R C ↔ D R B

Proof

Step Hyp Ref Expression
1 caovord.1 ⊢ A ∈ V
2 caovord.2 ⊢ B ∈ V
3 caovord.3 ⊢ z ∈ S → x R y ↔ z F x R z F y
4 caovord2.3 ⊢ C ∈ V
5 caovord2.com ⊢ x F y = y F x
6 caovord3.4 ⊢ D ∈ V
7 1 4 3 2 5 caovord2 ⊢ B ∈ S → A R C ↔ A F B R C F B
8 7 adantr ⊢ B ∈ S ∧ C ∈ 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 ∈ S ∧ C ∈ S ∧ A F B = C F D → A R C ↔ C F D R C F B
11 6 2 3 caovord ⊢ C ∈ S → D R B ↔ C F D R C F B
12 11 ad2antlr ⊢ B ∈ S ∧ C ∈ S ∧ A F B = C F D → D R B ↔ C F D R C F B
13 10 12 bitr4d ⊢ B ∈ S ∧ C ∈ S ∧ A F B = C F D → A R C ↔ D R B