Theorem relsdom 8942

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

Syntax hints:   ∖ cdif 3937  Rel wrel 5671   ≈ cen 8932   ≼ cdom 8933   ≺ csdm 8934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3943  df-in 3947  df-ss 3957  df-opab 5201  df-xp 5672  df-rel 5673  df-dom 8937  df-sdom 8938

This theorem is referenced by:  domdifsn  9050  sucdom2OLD  9078  sdom0OLD  9105  sdomirr  9110  sdomdif  9121  sucdom2  9202  0sdom1dom  9234  sdom1OLD  9239  1sdom2dom  9243  unxpdom  9249  unxpdom2  9250  sucxpdom  9251  isfinite2  9297  fin2inf  9305  card2on  9545  djuxpdom  10176  djufi  10177  infdif  10200  cfslb2n  10259  isfin5  10290  isfin6  10291  isfin4p1  10306  fin56  10384  fin67  10386  sdomsdomcard  10551  gchi  10615  canthp1lem1  10643  canthp1lem2  10644  canthp1  10645  frgpnabl  19785  fphpd  42043  sdomne0  42653  sdomne0d  42654