Theorem relsdom 8925

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

Syntax hints:   ∖ cdif 3911  Rel wrel 5643   ≈ cen 8915   ≼ cdom 8916   ≺ csdm 8917

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 3449  df-dif 3917  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-dom 8920  df-sdom 8921

This theorem is referenced by:  domdifsn  9024  sdomirr  9078  sdomdif  9089  sucdom2  9167  0sdom1dom  9185  sdom1OLD  9190  1sdom2dom  9194  unxpdom  9200  unxpdom2  9201  sucxpdom  9202  isfinite2  9245  fin2inf  9253  fodomfir  9279  card2on  9507  djuxpdom  10139  djufi  10140  infdif  10161  cfslb2n  10221  isfin5  10252  isfin6  10253  isfin4p1  10268  fin56  10346  fin67  10348  sdomsdomcard  10513  gchi  10577  canthp1lem1  10605  canthp1lem2  10606  canthp1  10607  frgpnabl  19805  fphpd  42804  sdomne0  43402  sdomne0d  43403