Theorem relsdom 8936

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 8935	. 2 ⊢ Rel ≼
2		reldif 5790	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8932	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5752	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 236	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3903  Rel wrel 5654   ≈ cen 8926   ≼ cdom 8927   ≺ csdm 8928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909  df-ss 3923  df-opab 5165  df-xp 5655  df-rel 5656  df-dom 8931  df-sdom 8932

This theorem is referenced by:  domdifsn  9034  sdomirr  9088  sdomdif  9099  sucdom2  9173  0sdom1dom  9192  1sdom2dom  9200  unxpdom  9205  unxpdom2  9206  sucxpdom  9207  isfinite2  9244  fin2inf  9250  fodomfir  9274  card2on  9504  djuxpdom  10144  djufi  10145  infdif  10166  cfslb2n  10227  isfin5  10258  isfin6  10259  isfin4p1  10274  fin56  10352  fin67  10354  sdomsdomcard  10519  gchi  10584  canthp1lem1  10612  canthp1lem2  10613  canthp1  10614  frgpnabl  19917  fphpd  43398  sdomne0  43994  sdomne0d  43995