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

Theorem cnvso 5485
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 5484 . . 3  |-  ( R  Po  A  <->  `' R  Po  A )
2 ralcom 2987 . . . 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 3081 . . . . . . 7  |-  y  e. 
_V
4 vex 3081 . . . . . . 7  |-  x  e. 
_V
53, 4brcnv 5131 . . . . . 6  |-  ( y `' R x  <->  x R
y )
6 equcom 1734 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
74, 3brcnv 5131 . . . . . 6  |-  ( x `' R y  <->  y R x )
85, 6, 73orbi123i 1178 . . . . 5  |-  ( ( y `' R x  \/  y  =  x  \/  x `' R
y )  <->  ( x R y  \/  x  =  y  \/  y R x ) )
982ralbii 2840 . . . 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 697 . 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 4751 . 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 4751 . 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 369    \/ w3o 964   A.wral 2799   class class class wbr 4401    Po wpo 4748    Or wor 4749   `'ccnv 4948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-po 4750  df-so 4751  df-cnv 4957
This theorem is referenced by:  wofib  7871  oemapso  8002  cflim2  8544  fin23lem40  8632  gtso  9568  infmxrcl  11391  infmxrlb  11408  infmxrgelb  11409  xrinfm0  11411  limsupval  13071  ramval  14188  ramcl2lem  14189  imasdsfn  14572  imasdsval  14573  nmoval  20427  metdsval  20556  ovolval  21090  ovolf  21098  xrge0infssd  26206  tosglb  26277  xrsclat  26287  xrge0iifiso  26511  omsfval  26854  oms0  26855  ballotlemi  27028  ballotlemiex  27029  ballotlemsup  27032  ballotlemimin  27033  ballotlemfrcn0  27057  ballotlemirc  27059  erdszelem9  27232  erdszelem11  27234  inffz  27532  heicant  28575  gtinf  28663  welb  28779  rencldnfilem  29308  pellfundval  29370  dgraaval  29650  dgraaf  29653  infrglb  29920
  Copyright terms: Public domain W3C validator