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

Theorem relsdom 6870
Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)
Assertion
Ref Expression
relsdom  |-  Rel  ~<

Proof of Theorem relsdom
StepHypRef Expression
1 reldom 6869 . 2  |-  Rel  ~<_
2 reldif 4805 . . 3  |-  ( Rel  ~<_  ->  Rel  (  ~<_  \  ~~  ) )
3 df-sdom 6866 . . . 4  |-  ~<  =  (  ~<_  \  ~~  )
43releqi 4772 . . 3  |-  ( Rel 
~< 
<->  Rel  (  ~<_  \  ~~  ) )
52, 4sylibr 203 . 2  |-  ( Rel  ~<_  ->  Rel  ~<  )
61, 5ax-mp 8 1  |-  Rel  ~<
Colors of variables: wff set class
Syntax hints:    \ cdif 3149   Rel wrel 4694    ~~ cen 6860    ~<_ cdom 6861    ~< csdm 6862
This theorem is referenced by:  domdifsn  6945  sdom0  6993  sdomirr  6998  sdomdif  7009  sucdom2  7057  sdom1  7062  unxpdom  7070  unxpdom2  7071  sucxpdom  7072  isfinite2  7115  fin2inf  7120  card2on  7268  cdaxpdom  7815  cdafi  7816  cfslb2n  7894  isfin5  7925  isfin6  7926  isfin4-3  7941  fin56  8019  fin67  8021  sdomsdomcard  8182  gchi  8246  canthp1lem1  8274  canthp1lem2  8275  canthp1  8276  frgpnabl  15163  fphpd  26899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-rel 4696  df-dom 6865  df-sdom 6866
  Copyright terms: Public domain W3C validator