Theorem relsdom 8946

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 8945	. 2 ⊢ Rel ≼
2		reldif 5802	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8942	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5764	. . 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 3902  Rel wrel 5666   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922  df-opab 5174  df-xp 5667  df-rel 5668  df-dom 8941  df-sdom 8942

This theorem is used by:  domdifsn  9044  sdomirr  9098  sdomdif  9109  sucdom2  9183  0sdom1dom  9202  1sdom2dom  9210  unxpdom  9215  unxpdom2  9216  sucxpdom  9217  isfinite2  9254  fin2inf  9260  fodomfir  9283  card2on  9512  djuxpdom  10174  djufi  10175  infdif  10196  cfslb2n  10256  isfin5  10287  isfin6  10288  isfin4p1  10303  fin56  10381  fin67  10383  sdomsdomcard  10548  gchi  10613  canthp1lem1  10641  canthp1lem2  10642  canthp1  10643  frgpnabl  19949  kardsdom  35583  fphpd  43571  sdomne0  44167  sdomne0d  44168