Theorem relsdom 8956

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

This proof depends on syntax axioms:   ∖ cdif 3903  Rel wrel 5668   ≈ cen 8946   ≼ cdom 8947   ≺ csdm 8948

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923  df-opab 5176  df-xp 5669  df-rel 5670  df-dom 8951  df-sdom 8952

This theorem is used by:  domdifsn  9055  sdomirr  9109  sdomdif  9120  sucdom2  9194  0sdom1dom  9213  1sdom2dom  9221  unxpdom  9226  unxpdom2  9227  sucxpdom  9228  isfinite2  9265  fin2inf  9271  fodomfir  9294  card2on  9523  djuxpdom  10185  djufi  10186  infdif  10207  cfslb2n  10267  isfin5  10298  isfin6  10299  isfin4p1  10314  fin56  10392  fin67  10394  sdomsdomcard  10563  gchi  10628  canthp1lem1  10656  canthp1lem2  10657  canthp1  10658  frgpnabl  19993  kardsdom  35636  fphpd  43620  sdomne0  44216  sdomne0d  44217