Theorem relsdom 8876

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

Syntax hints:   ∖ cdif 3894  Rel wrel 5619   ≈ cen 8866   ≼ cdom 8867   ≺ csdm 8868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-dom 8871  df-sdom 8872

This theorem is referenced by:  domdifsn  8973  sdomirr  9027  sdomdif  9038  sucdom2  9112  0sdom1dom  9130  1sdom2dom  9138  unxpdom  9143  unxpdom2  9144  sucxpdom  9145  isfinite2  9182  fin2inf  9188  fodomfir  9212  card2on  9440  djuxpdom  10077  djufi  10078  infdif  10099  cfslb2n  10159  isfin5  10190  isfin6  10191  isfin4p1  10206  fin56  10284  fin67  10286  sdomsdomcard  10451  gchi  10515  canthp1lem1  10543  canthp1lem2  10544  canthp1  10545  frgpnabl  19787  fphpd  42908  sdomne0  43505  sdomne0d  43506