Theorem relsdom 8948

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

Syntax hints:   ∖ cdif 3945  Rel wrel 5681   ≈ cen 8938   ≼ cdom 8939   ≺ csdm 8940

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-dom 8943  df-sdom 8944

This theorem is referenced by:  domdifsn  9056  sucdom2OLD  9084  sdom0OLD  9111  sdomirr  9116  sdomdif  9127  sucdom2  9208  0sdom1dom  9240  sdom1OLD  9245  1sdom2dom  9249  unxpdom  9255  unxpdom2  9256  sucxpdom  9257  isfinite2  9303  fin2inf  9311  card2on  9551  djuxpdom  10182  djufi  10183  infdif  10206  cfslb2n  10265  isfin5  10296  isfin6  10297  isfin4p1  10312  fin56  10390  fin67  10392  sdomsdomcard  10557  gchi  10621  canthp1lem1  10649  canthp1lem2  10650  canthp1  10651  frgpnabl  19784  fphpd  41856  sdomne0  42466  sdomne0d  42467