Theorem relsdom 8950

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 8949	. 2 ⊢ Rel ≼
2		reldif 5803	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8946	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5765	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 237	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3910  Rel wrel 5667   ≈ cen 8940   ≼ cdom 8941   ≺ csdm 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930  df-opab 5178  df-xp 5668  df-rel 5669  df-dom 8945  df-sdom 8946

This theorem is referenced by:  domdifsn  9048  sdomirr  9102  sdomdif  9113  sucdom2  9187  0sdom1dom  9206  1sdom2dom  9214  unxpdom  9219  unxpdom2  9220  sucxpdom  9221  isfinite2  9258  fin2inf  9264  fodomfir  9287  card2on  9516  djuxpdom  10169  djufi  10170  infdif  10191  cfslb2n  10252  isfin5  10283  isfin6  10284  isfin4p1  10299  fin56  10377  fin67  10379  sdomsdomcard  10544  gchi  10609  canthp1lem1  10637  canthp1lem2  10638  canthp1  10639  frgpnabl  19945  kardsdom  35508  fphpd  43469  sdomne0  44065  sdomne0d  44066