Theorem relsdom 8891

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 8890	. 2 ⊢ Rel ≼
2		reldif 5759	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8887	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5722	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 235	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3880  Rel wrel 5624   ≈ cen 8881   ≼ cdom 8882   ≺ csdm 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-ss 3900  df-opab 5136  df-xp 5625  df-rel 5626  df-dom 8886  df-sdom 8887

This theorem is referenced by:  domdifsn  8989  sdomirr  9043  sdomdif  9054  sucdom2  9128  0sdom1dom  9147  1sdom2dom  9155  unxpdom  9160  unxpdom2  9161  sucxpdom  9162  isfinite2  9199  fin2inf  9205  fodomfir  9229  card2on  9460  djuxpdom  10100  djufi  10101  infdif  10122  cfslb2n  10182  isfin5  10213  isfin6  10214  isfin4p1  10229  fin56  10307  fin67  10309  sdomsdomcard  10474  gchi  10539  canthp1lem1  10567  canthp1lem2  10568  canthp1  10569  frgpnabl  19842  fphpd  43270  sdomne0  43866  sdomne0d  43867