Theorem relsdom 8946

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

Syntax hints:   ∖ cdif 3946  Rel wrel 5682   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-dom 8941  df-sdom 8942

This theorem is referenced by:  domdifsn  9054  sucdom2OLD  9082  sdom0OLD  9109  sdomirr  9114  sdomdif  9125  sucdom2  9206  0sdom1dom  9238  sdom1OLD  9243  1sdom2dom  9247  unxpdom  9253  unxpdom2  9254  sucxpdom  9255  isfinite2  9301  fin2inf  9309  card2on  9549  djuxpdom  10180  djufi  10181  infdif  10204  cfslb2n  10263  isfin5  10294  isfin6  10295  isfin4p1  10310  fin56  10388  fin67  10390  sdomsdomcard  10555  gchi  10619  canthp1lem1  10647  canthp1lem2  10648  canthp1  10649  frgpnabl  19743  fphpd  41554  sdomne0  42164  sdomne0d  42165