Theorem relsdom 8991

Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)

Assertion

Ref	Expression
relsdom	⊢ Rel ≺

Proof of Theorem relsdom

Step	Hyp	Ref	Expression
1		reldom 8990	. 2 ⊢ Rel ≼
2		reldif 5828	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8987	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5790	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 234	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3960  Rel wrel 5694   ≈ cen 8981   ≼ cdom 8982   ≺ csdm 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-ss 3980  df-opab 5211  df-xp 5695  df-rel 5696  df-dom 8986  df-sdom 8987

This theorem is referenced by:  domdifsn  9093  sucdom2OLD  9121  sdom0OLD  9148  sdomirr  9153  sdomdif  9164  sucdom2  9241  0sdom1dom  9272  sdom1OLD  9277  1sdom2dom  9281  unxpdom  9287  unxpdom2  9288  sucxpdom  9289  isfinite2  9332  fin2inf  9340  fodomfir  9366  card2on  9592  djuxpdom  10224  djufi  10225  infdif  10246  cfslb2n  10306  isfin5  10337  isfin6  10338  isfin4p1  10353  fin56  10431  fin67  10433  sdomsdomcard  10598  gchi  10662  canthp1lem1  10690  canthp1lem2  10691  canthp1  10692  frgpnabl  19908  fphpd  42804  sdomne0  43403  sdomne0d  43404