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

Theorem relsdom 8993
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 8992 . 2 Rel ≼
2 reldif 5824 . . 3 (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3 df-sdom 8989 . . . 4 ≺ = ( ≼ ∖ ≈ )
43releqi 5786 . . 3 (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
52, 4sylibr 234 . 2 (Rel ≼ → Rel ≺ )
61, 5ax-mp 5 1 Rel ≺
Colors of variables: wff setvar class
Syntax hints:  cdif 3947  Rel wrel 5689  cen 8983  cdom 8984  csdm 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-ss 3967  df-opab 5205  df-xp 5690  df-rel 5691  df-dom 8988  df-sdom 8989
This theorem is referenced by:  domdifsn  9095  sucdom2OLD  9123  sdom0OLD  9150  sdomirr  9155  sdomdif  9166  sucdom2  9244  0sdom1dom  9275  sdom1OLD  9280  1sdom2dom  9284  unxpdom  9290  unxpdom2  9291  sucxpdom  9292  isfinite2  9335  fin2inf  9343  fodomfir  9369  card2on  9595  djuxpdom  10227  djufi  10228  infdif  10249  cfslb2n  10309  isfin5  10340  isfin6  10341  isfin4p1  10356  fin56  10434  fin67  10436  sdomsdomcard  10601  gchi  10665  canthp1lem1  10693  canthp1lem2  10694  canthp1  10695  frgpnabl  19894  fphpd  42832  sdomne0  43431  sdomne0d  43432
  Copyright terms: Public domain W3C validator