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

Theorem cnvso 5537
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 5536 . . 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 5176 . . . . . 6  |-  ( y `' R x  <->  x R
y )
6 equcom 1738 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
74, 3brcnv 5176 . . . . . 6  |-  ( x `' R y  <->  y R x )
85, 6, 73orbi123i 1181 . . . . 5  |-  ( ( y `' R x  \/  y  =  x  \/  x `' R
y )  <->  ( x R y  \/  x  =  y  \/  y R x ) )
982ralbii 2889 . . . 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 4794 . 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 4794 . 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 967   A.wral 2807   class class class wbr 4440    Po wpo 4791    Or wor 4792   `'ccnv 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-po 4793  df-so 4794  df-cnv 5000
This theorem is referenced by:  wofib  7959  oemapso  8090  cflim2  8632  fin23lem40  8720  gtso  9655  infmxrcl  11497  infmxrlb  11514  infmxrgelb  11515  xrinfm0  11517  limsupval  13246  ramval  14374  ramcl2lem  14375  imasdsfn  14758  imasdsval  14759  nmoval  20950  metdsval  21079  ovolval  21613  ovolf  21621  xrge0infssd  27235  tosglb  27306  xrsclat  27316  xrge0iifiso  27539  omsfval  27891  oms0  27892  ballotlemi  28065  ballotlemiex  28066  ballotlemsup  28069  ballotlemimin  28070  ballotlemfrcn0  28094  ballotlemirc  28096  erdszelem9  28269  erdszelem11  28271  inffz  28569  heicant  29613  gtinf  29701  welb  29817  rencldnfilem  30345  pellfundval  30407  dgraaval  30687  dgraaf  30690  infrglb  31095  fourierdlem42  31404
  Copyright terms: Public domain W3C validator