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

Theorem relsdom 8740
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 8739 . 2 Rel ≼
2 reldif 5725 . . 3 (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3 df-sdom 8736 . . . 4 ≺ = ( ≼ ∖ ≈ )
43releqi 5688 . . 3 (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
52, 4sylibr 233 . 2 (Rel ≼ → Rel ≺ )
61, 5ax-mp 5 1 Rel ≺
Colors of variables: wff setvar class
Syntax hints:  cdif 3884  Rel wrel 5594  cen 8730  cdom 8731  csdm 8732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-dom 8735  df-sdom 8736
This theorem is referenced by:  domdifsn  8841  sucdom2OLD  8869  sdom0OLD  8896  sdomirr  8901  sdomdif  8912  sucdom2  8989  sdom1  9022  unxpdom  9030  unxpdom2  9031  sucxpdom  9032  isfinite2  9072  fin2inf  9077  card2on  9313  djuxpdom  9941  djufi  9942  infdif  9965  cfslb2n  10024  isfin5  10055  isfin6  10056  isfin4p1  10071  fin56  10149  fin67  10151  sdomsdomcard  10316  gchi  10380  canthp1lem1  10408  canthp1lem2  10409  canthp1  10410  frgpnabl  19476  fphpd  40638
  Copyright terms: Public domain W3C validator