Theorem relsdom 8980

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 8979	. 2 ⊢ Rel ≼
2		reldif 5793	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8976	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5754	. . 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 5656   ≈ cen 8970   ≼ cdom 8971   ≺ csdm 8972

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-dom 8975  df-sdom 8976

This theorem is used by:  domdifsn  9079  sdomirr  9133  sdomdif  9144  sucdom2  9218  0sdom1dom  9237  1sdom2dom  9245  unxpdom  9250  unxpdom2  9251  sucxpdom  9252  isfinite2  9290  fin2inf  9296  fodomfir  9319  card2on  9548  djuxpdom  10264  djufi  10265  infdif  10286  cfslb2n  10346  isfin5  10377  isfin6  10378  isfin4p1  10393  fin56  10471  fin67  10473  sdomsdomcard  10644  gchi  10709  canthp1lem1  10737  canthp1lem2  10738  canthp1  10739  frgpnabl  20089  kardsdom  35830  fphpd  43822  sdomne0  44413  sdomne0d  44414