Theorem relsdom 8894

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

Syntax hints:   ∖ cdif 3899  Rel wrel 5630   ≈ cen 8884   ≼ cdom 8885   ≺ csdm 8886

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905  df-ss 3919  df-opab 5162  df-xp 5631  df-rel 5632  df-dom 8889  df-sdom 8890

This theorem is referenced by:  domdifsn  8992  sdomirr  9046  sdomdif  9057  sucdom2  9131  0sdom1dom  9150  1sdom2dom  9158  unxpdom  9163  unxpdom2  9164  sucxpdom  9165  isfinite2  9202  fin2inf  9208  fodomfir  9232  card2on  9463  djuxpdom  10100  djufi  10101  infdif  10122  cfslb2n  10182  isfin5  10213  isfin6  10214  isfin4p1  10229  fin56  10307  fin67  10309  sdomsdomcard  10474  gchi  10539  canthp1lem1  10567  canthp1lem2  10568  canthp1  10569  frgpnabl  19808  fphpd  43125  sdomne0  43721  sdomne0d  43722