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

Theorem cnvso 5414
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 5413 . . 3  |-  ( R  Po  A  <->  `' R  Po  A )
2 ralcom 2870 . . . 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 2961 . . . . . . 7  |-  y  e. 
_V
4 vex 2961 . . . . . . 7  |-  x  e. 
_V
53, 4brcnv 5058 . . . . . 6  |-  ( y `' R x  <->  x R
y )
6 equcom 1693 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
74, 3brcnv 5058 . . . . . 6  |-  ( x `' R y  <->  y R x )
85, 6, 73orbi123i 1144 . . . . 5  |-  ( ( y `' R x  \/  y  =  x  \/  x `' R
y )  <->  ( x R y  \/  x  =  y  \/  y R x ) )
982ralbii 2733 . . . 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 245 . . 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 680 . 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 4507 . 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 4507 . 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 270 1  |-  ( R  Or  A  <->  `' R  Or  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    \/ w3o 936   A.wral 2707   class class class wbr 4215    Po wpo 4504    Or wor 4505   `'ccnv 4880
This theorem is referenced by:  wofib  7517  oemapso  7641  cflim2  8148  fin23lem40  8236  lbinfm  9966  infmsup  9991  infmrgelb  9993  infmrlb  9994  infmxrcl  10900  infmxrlb  10917  infmxrgelb  10918  xrinfm0  10920  limsupval  12273  odzval  13182  ramval  13381  ramcl2lem  13382  imasdsfn  13745  imasdsval  13746  odval  15177  odf  15180  gexval  15217  nmoval  18754  metdsval  18882  ovolval  19375  ovolf  19383  dvlt0  19894  elqaalem1  20241  elqaalem3  20243  aalioulem2  20255  tosglb  24197  xrge0iifiso  24326  ballotlemi  24763  ballotlemiex  24764  ballotlemsup  24767  ballotlemimin  24768  ballotlemfrcn0  24792  ballotlemirc  24794  erdszelem9  24890  erdszelem11  24892  inffz  25205  heicant  26253  gtinf  26336  welb  26452  rencldnfilem  26895  pellfundval  26957  dgraaval  27340  dgraaf  27343  infrglb  27712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-po 4506  df-so 4507  df-cnv 4889
  Copyright terms: Public domain W3C validator