Theorem relsdom 8879

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

Syntax hints:   ∖ cdif 3900  Rel wrel 5624   ≈ cen 8869   ≼ cdom 8870   ≺ csdm 8871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626  df-dom 8874  df-sdom 8875

This theorem is referenced by:  domdifsn  8977  sdomirr  9031  sdomdif  9042  sucdom2  9117  0sdom1dom  9135  1sdom2dom  9143  unxpdom  9148  unxpdom2  9149  sucxpdom  9150  isfinite2  9187  fin2inf  9193  fodomfir  9218  card2on  9446  djuxpdom  10080  djufi  10081  infdif  10102  cfslb2n  10162  isfin5  10193  isfin6  10194  isfin4p1  10209  fin56  10287  fin67  10289  sdomsdomcard  10454  gchi  10518  canthp1lem1  10546  canthp1lem2  10547  canthp1  10548  frgpnabl  19754  fphpd  42799  sdomne0  43396  sdomne0d  43397