Theorem relsdom 8740

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 8739	. 2 ⊢ Rel ≼
2		reldif 5725	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8736	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5688	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 233	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3884  Rel wrel 5594   ≈ cen 8730   ≼ cdom 8731   ≺ csdm 8732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-dom 8735  df-sdom 8736

This theorem is referenced by:  domdifsn  8841  sucdom2OLD  8869  sdom0OLD  8896  sdomirr  8901  sdomdif  8912  sucdom2  8989  sdom1  9022  unxpdom  9030  unxpdom2  9031  sucxpdom  9032  isfinite2  9072  fin2inf  9077  card2on  9313  djuxpdom  9941  djufi  9942  infdif  9965  cfslb2n  10024  isfin5  10055  isfin6  10056  isfin4p1  10071  fin56  10149  fin67  10151  sdomsdomcard  10316  gchi  10380  canthp1lem1  10408  canthp1lem2  10409  canthp1  10410  frgpnabl  19476  fphpd  40638