Theorem relsdom 9010

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

Syntax hints:   ∖ cdif 3973  Rel wrel 5705   ≈ cen 9000   ≼ cdom 9001   ≺ csdm 9002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-dom 9005  df-sdom 9006

This theorem is referenced by:  domdifsn  9120  sucdom2OLD  9148  sdom0OLD  9175  sdomirr  9180  sdomdif  9191  sucdom2  9269  0sdom1dom  9301  sdom1OLD  9306  1sdom2dom  9310  unxpdom  9316  unxpdom2  9317  sucxpdom  9318  isfinite2  9362  fin2inf  9370  fodomfir  9396  card2on  9623  djuxpdom  10255  djufi  10256  infdif  10277  cfslb2n  10337  isfin5  10368  isfin6  10369  isfin4p1  10384  fin56  10462  fin67  10464  sdomsdomcard  10629  gchi  10693  canthp1lem1  10721  canthp1lem2  10722  canthp1  10723  frgpnabl  19917  fphpd  42772  sdomne0  43375  sdomne0d  43376