Theorem relsdom 8964

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 8963	. 2 ⊢ Rel ≼
2		reldif 5794	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8960	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5756	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 234	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3923  Rel wrel 5659   ≈ cen 8954   ≼ cdom 8955   ≺ csdm 8956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-dom 8959  df-sdom 8960

This theorem is referenced by:  domdifsn  9066  sucdom2OLD  9094  sdom0OLD  9121  sdomirr  9126  sdomdif  9137  sucdom2  9215  0sdom1dom  9244  sdom1OLD  9249  1sdom2dom  9253  unxpdom  9259  unxpdom2  9260  sucxpdom  9261  isfinite2  9304  fin2inf  9312  fodomfir  9338  card2on  9566  djuxpdom  10198  djufi  10199  infdif  10220  cfslb2n  10280  isfin5  10311  isfin6  10312  isfin4p1  10327  fin56  10405  fin67  10407  sdomsdomcard  10572  gchi  10636  canthp1lem1  10664  canthp1lem2  10665  canthp1  10666  frgpnabl  19854  fphpd  42786  sdomne0  43384  sdomne0d  43385