MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvso Structured version   Unicode version

Theorem cnvso 5529
Description: The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.)
Assertion
Ref Expression
cnvso  |-  ( R  Or  A  <->  `' R  Or  A )

Proof of Theorem cnvso
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvpo 5528 . . 3  |-  ( R  Po  A  <->  `' R  Po  A )
2 ralcom 3015 . . . 4  |-  ( 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 3109 . . . . . . 7  |-  y  e. 
_V
4 vex 3109 . . . . . . 7  |-  x  e. 
_V
53, 4brcnv 5174 . . . . . 6  |-  ( y `' R x  <->  x R
y )
6 equcom 1799 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
74, 3brcnv 5174 . . . . . 6  |-  ( x `' R y  <->  y R x )
85, 6, 73orbi123i 1184 . . . . 5  |-  ( ( y `' R x  \/  y  =  x  \/  x `' R
y )  <->  ( x R y  \/  x  =  y  \/  y R x ) )
982ralbii 2886 . . . 4  |-  ( 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 ) )
102, 9bitr4i 252 . . 3  |-  ( 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 ) )
111, 10anbi12i 695 . 2  |-  ( ( 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 4790 . 2  |-  ( 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 4790 . 2  |-  ( `' R  Or  A  <->  ( `' R  Po  A  /\  A. y  e.  A  A. x  e.  A  (
y `' R x  \/  y  =  x  \/  x `' R
y ) ) )
1411, 12, 133bitr4i 277 1  |-  ( R  Or  A  <->  `' R  Or  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    \/ w3o 970   A.wral 2804   class class class wbr 4439    Po wpo 4787    Or wor 4788   `'ccnv 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-po 4789  df-so 4790  df-cnv 4996
This theorem is referenced by:  wofib  7962  oemapso  8092  cflim2  8634  fin23lem40  8722  gtso  9655  infmxrcl  11511  infmxrlb  11528  infmxrgelb  11529  xrinfm0  11531  limsupval  13382  ramval  14613  ramcl2lem  14614  imasdsfn  15006  imasdsval  15007  nmoval  21391  metdsval  21520  ovolval  22054  ovolf  22062  xrge0infssd  27815  tosglb  27895  xrsclat  27905  xrge0iifiso  28155  omsfval  28505  omsf  28507  oms0  28508  omssubaddlem  28510  omssubadd  28511  inffz  29352  welb  30470  fourierdlem42  32173
  Copyright terms: Public domain W3C validator