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

Proof

Step Hyp Ref Expression
1 cnvpo 
 |-  ( R Po A <-> `' R Po A )
2 ralcom 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A A. x e. A ( x R y \/ x = y \/ y R x ) )
3 vex 
 |-  y e. _V
4 vex 
 |-  x e. _V
5 3 4 brcnv 
 |-  ( y `' R x <-> x R y )
6 equcom 
 |-  ( y = x <-> x = y )
7 4 3 brcnv 
 |-  ( x `' R y <-> y R x )
8 5 6 7 3orbi123i 
 |-  ( ( y `' R x \/ y = x \/ x `' R y ) <-> ( x R y \/ x = y \/ y R x ) )
9 8 2ralbii 
 |-  ( A. y e. A A. x e. A ( y `' R x \/ y = x \/ x `' R y ) <-> A. y e. A A. x e. A ( x R y \/ x = y \/ y R x ) )
10 2 9 bitr4i 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A A. x e. A ( y `' R x \/ y = x \/ x `' R y ) )
11 1 10 anbi12i 
 |-  ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) <-> ( `' R Po A /\ A. y e. A A. x e. A ( y `' R x \/ y = x \/ x `' R y ) ) )
12 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
13 df-so 
 |-  ( `' R Or A <-> ( `' R Po A /\ A. y e. A A. x e. A ( y `' R x \/ y = x \/ x `' R y ) ) )
14 11 12 13 3bitr4i 
 |-  ( R Or A <-> `' R Or A )