Theorem relsdom 8900

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

Syntax hints:   ∖ cdif 3886  Rel wrel 5636   ≈ cen 8890   ≼ cdom 8891   ≺ csdm 8892

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-dom 8895  df-sdom 8896

This theorem is referenced by:  domdifsn  8998  sdomirr  9052  sdomdif  9063  sucdom2  9137  0sdom1dom  9156  1sdom2dom  9164  unxpdom  9169  unxpdom2  9170  sucxpdom  9171  isfinite2  9208  fin2inf  9214  fodomfir  9238  card2on  9469  djuxpdom  10108  djufi  10109  infdif  10130  cfslb2n  10190  isfin5  10221  isfin6  10222  isfin4p1  10237  fin56  10315  fin67  10317  sdomsdomcard  10482  gchi  10547  canthp1lem1  10575  canthp1lem2  10576  canthp1  10577  frgpnabl  19850  fphpd  43244  sdomne0  43840  sdomne0d  43841