Theorem relsdom 8888

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

Syntax hints:   ∖ cdif 3896  Rel wrel 5627   ≈ cen 8878   ≼ cdom 8879   ≺ csdm 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916  df-opab 5159  df-xp 5628  df-rel 5629  df-dom 8883  df-sdom 8884

This theorem is referenced by:  domdifsn  8986  sdomirr  9040  sdomdif  9051  sucdom2  9125  0sdom1dom  9144  1sdom2dom  9152  unxpdom  9157  unxpdom2  9158  sucxpdom  9159  isfinite2  9196  fin2inf  9202  fodomfir  9226  card2on  9457  djuxpdom  10094  djufi  10095  infdif  10116  cfslb2n  10176  isfin5  10207  isfin6  10208  isfin4p1  10223  fin56  10301  fin67  10303  sdomsdomcard  10468  gchi  10533  canthp1lem1  10561  canthp1lem2  10562  canthp1  10563  frgpnabl  19802  fphpd  43000  sdomne0  43596  sdomne0d  43597