Theorem relsdom 8499

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 8498	. 2 ⊢ Rel ≼
2		reldif 5652	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8495	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5616	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 237	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3878  Rel wrel 5524   ≈ cen 8489   ≼ cdom 8490   ≺ csdm 8491

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526  df-dom 8494  df-sdom 8495

This theorem is referenced by:  domdifsn  8583  sucdom2  8610  sdom0  8633  sdomirr  8638  sdomdif  8649  sdom1  8702  unxpdom  8709  unxpdom2  8710  sucxpdom  8711  isfinite2  8760  fin2inf  8765  card2on  9002  djuxpdom  9596  djufi  9597  infdif  9620  cfslb2n  9679  isfin5  9710  isfin6  9711  isfin4p1  9726  fin56  9804  fin67  9806  sdomsdomcard  9971  gchi  10035  canthp1lem1  10063  canthp1lem2  10064  canthp1  10065  frgpnabl  18988  fphpd  39757