This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvso

Description: The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005)

Ref Expression
Assertion cnvso ⊢ R Or A ↔ R -1 Or A

Proof

Step Hyp Ref Expression
1 cnvpo ⊢ R Po A ↔ R -1 Po A
2 ralcom ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ ∀ y ∈ A ∀ x ∈ A x R y ∨ x = y ∨ y R x
3 vex ⊢ y ∈ V
4 vex ⊢ x ∈ V
5 3 4 brcnv ⊢ y R -1 x ↔ x R y
6 equcom ⊢ y = x ↔ x = y
7 4 3 brcnv ⊢ x R -1 y ↔ y R x
8 5 6 7 3orbi123i ⊢ y R -1 x ∨ y = x ∨ x R -1 y ↔ x R y ∨ x = y ∨ y R x
9 8 2ralbii ⊢ ∀ y ∈ A ∀ x ∈ A y R -1 x ∨ y = x ∨ x R -1 y ↔ ∀ y ∈ A ∀ x ∈ A x R y ∨ x = y ∨ y R x
10 2 9 bitr4i ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ ∀ y ∈ A ∀ x ∈ A y R -1 x ∨ y = x ∨ x R -1 y
11 1 10 anbi12i ⊢ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ R -1 Po A ∧ ∀ y ∈ A ∀ x ∈ A y R -1 x ∨ y = x ∨ x R -1 y
12 df-so ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
13 df-so ⊢ R -1 Or A ↔ R -1 Po A ∧ ∀ y ∈ A ∀ x ∈ A y R -1 x ∨ y = x ∨ x R -1 y
14 11 12 13 3bitr4i ⊢ R Or A ↔ R -1 Or A