Theorem relsdom 8698

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

Syntax hints:   ∖ cdif 3880  Rel wrel 5585   ≈ cen 8688   ≼ cdom 8689   ≺ csdm 8690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-dom 8693  df-sdom 8694

This theorem is referenced by:  domdifsn  8795  sucdom2  8822  sdom0  8845  sdomirr  8850  sdomdif  8861  sdom1  8952  unxpdom  8959  unxpdom2  8960  sucxpdom  8961  isfinite2  9002  fin2inf  9007  card2on  9243  djuxpdom  9872  djufi  9873  infdif  9896  cfslb2n  9955  isfin5  9986  isfin6  9987  isfin4p1  10002  fin56  10080  fin67  10082  sdomsdomcard  10247  gchi  10311  canthp1lem1  10339  canthp1lem2  10340  canthp1  10341  frgpnabl  19391  fphpd  40554