Metamath Proof Explorer

Theorem soeq1

Description: Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997)

Ref Expression
Assertion soeq1 ⊢ R = S → R Or A ↔ S Or A

Proof

Step Hyp Ref Expression
1 poeq1 ⊢ R = S → R Po A ↔ S Po A
2 breq ⊢ R = S → x R y ↔ x S y
3 biidd ⊢ R = S → x = y ↔ x = y
4 breq ⊢ R = S → y R x ↔ y S x
5 2 3 4 3orbi123d ⊢ R = S → x R y ∨ x = y ∨ y R x ↔ x S y ∨ x = y ∨ y S x
6 5 2ralbidv ⊢ R = S → ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ ∀ x ∈ A ∀ y ∈ A x S y ∨ x = y ∨ y S x
7 1 6 anbi12d ⊢ R = S → R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ S Po A ∧ ∀ x ∈ A ∀ y ∈ A x S y ∨ x = y ∨ y S x
8 df-so ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
9 df-so ⊢ S Or A ↔ S Po A ∧ ∀ x ∈ A ∀ y ∈ A x S y ∨ x = y ∨ y S x
10 7 8 9 3bitr4g ⊢ R = S → R Or A ↔ S Or A