Theorem relsdom 8963

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 8962	. 2 ⊢ Rel ≼
2		reldif 5797	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8959	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5758	. . 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 3896  Rel wrel 5660   ≈ cen 8953   ≼ cdom 8954   ≺ csdm 8955

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916  df-opab 5168  df-xp 5661  df-rel 5662  df-dom 8958  df-sdom 8959

This theorem is used by:  domdifsn  9062  sdomirr  9116  sdomdif  9127  sucdom2  9201  0sdom1dom  9220  1sdom2dom  9228  unxpdom  9233  unxpdom2  9234  sucxpdom  9235  isfinite2  9272  fin2inf  9278  fodomfir  9301  card2on  9530  djuxpdom  10210  djufi  10211  infdif  10232  cfslb2n  10292  isfin5  10323  isfin6  10324  isfin4p1  10339  fin56  10417  fin67  10419  sdomsdomcard  10590  gchi  10655  canthp1lem1  10683  canthp1lem2  10684  canthp1  10685  frgpnabl  20025  kardsdom  35718  fphpd  43671  sdomne0  44267  sdomne0d  44268