Theorem relsdom 8993

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

Syntax hints:   ∖ cdif 3947  Rel wrel 5689   ≈ cen 8983   ≼ cdom 8984   ≺ csdm 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-ss 3967  df-opab 5205  df-xp 5690  df-rel 5691  df-dom 8988  df-sdom 8989

This theorem is referenced by:  domdifsn  9095  sucdom2OLD  9123  sdom0OLD  9150  sdomirr  9155  sdomdif  9166  sucdom2  9244  0sdom1dom  9275  sdom1OLD  9280  1sdom2dom  9284  unxpdom  9290  unxpdom2  9291  sucxpdom  9292  isfinite2  9335  fin2inf  9343  fodomfir  9369  card2on  9595  djuxpdom  10227  djufi  10228  infdif  10249  cfslb2n  10309  isfin5  10340  isfin6  10341  isfin4p1  10356  fin56  10434  fin67  10436  sdomsdomcard  10601  gchi  10665  canthp1lem1  10693  canthp1lem2  10694  canthp1  10695  frgpnabl  19894  fphpd  42832  sdomne0  43431  sdomne0d  43432