Theorem relsdom 8902

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

Syntax hints:   ∖ cdif 3908  Rel wrel 5636   ≈ cen 8892   ≼ cdom 8893   ≺ csdm 8894

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638  df-dom 8897  df-sdom 8898

This theorem is referenced by:  domdifsn  9001  sdomirr  9055  sdomdif  9066  sucdom2  9144  0sdom1dom  9162  1sdom2dom  9170  unxpdom  9176  unxpdom2  9177  sucxpdom  9178  isfinite2  9221  fin2inf  9229  fodomfir  9255  card2on  9483  djuxpdom  10115  djufi  10116  infdif  10137  cfslb2n  10197  isfin5  10228  isfin6  10229  isfin4p1  10244  fin56  10322  fin67  10324  sdomsdomcard  10489  gchi  10553  canthp1lem1  10581  canthp1lem2  10582  canthp1  10583  frgpnabl  19789  fphpd  42797  sdomne0  43395  sdomne0d  43396