Theorem relsdom 8904

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 8903	. 2 ⊢ Rel ≼
2		reldif 5774	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8900	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5737	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 234	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3900  Rel wrel 5639   ≈ cen 8894   ≼ cdom 8895   ≺ csdm 8896

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920  df-opab 5163  df-xp 5640  df-rel 5641  df-dom 8899  df-sdom 8900

This theorem is referenced by:  domdifsn  9002  sdomirr  9056  sdomdif  9067  sucdom2  9141  0sdom1dom  9160  1sdom2dom  9168  unxpdom  9173  unxpdom2  9174  sucxpdom  9175  isfinite2  9212  fin2inf  9218  fodomfir  9242  card2on  9473  djuxpdom  10110  djufi  10111  infdif  10132  cfslb2n  10192  isfin5  10223  isfin6  10224  isfin4p1  10239  fin56  10317  fin67  10319  sdomsdomcard  10484  gchi  10549  canthp1lem1  10577  canthp1lem2  10578  canthp1  10579  frgpnabl  19821  fphpd  43202  sdomne0  43798  sdomne0d  43799