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

Theorem relsdom 8120
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 8119 . 2 Rel ≼
2 reldif 5376 . . 3 (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3 df-sdom 8116 . . . 4 ≺ = ( ≼ ∖ ≈ )
43releqi 5341 . . 3 (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
52, 4sylibr 224 . 2 (Rel ≼ → Rel ≺ )
61, 5ax-mp 5 1 Rel ≺
Colors of variables: wff setvar class
Syntax hints:  cdif 3720  Rel wrel 5255  cen 8110  cdom 8111  csdm 8112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-opab 4848  df-xp 5256  df-rel 5257  df-dom 8115  df-sdom 8116
This theorem is referenced by:  domdifsn  8203  sdom0  8252  sdomirr  8257  sdomdif  8268  sucdom2  8316  sdom1  8320  unxpdom  8327  unxpdom2  8328  sucxpdom  8329  isfinite2  8378  fin2inf  8383  card2on  8619  cdaxpdom  9217  cdafi  9218  cfslb2n  9296  isfin5  9327  isfin6  9328  isfin4-3  9343  fin56  9421  fin67  9423  sdomsdomcard  9588  gchi  9652  canthp1lem1  9680  canthp1lem2  9681  canthp1  9682  frgpnabl  18485  fphpd  37906
  Copyright terms: Public domain W3C validator