Theorem relsdom 8971

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

Syntax hints:   ∖ cdif 3928  Rel wrel 5664   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-ss 3948  df-opab 5187  df-xp 5665  df-rel 5666  df-dom 8966  df-sdom 8967

This theorem is referenced by:  domdifsn  9073  sucdom2OLD  9101  sdom0OLD  9128  sdomirr  9133  sdomdif  9144  sucdom2  9222  0sdom1dom  9251  sdom1OLD  9256  1sdom2dom  9260  unxpdom  9266  unxpdom2  9267  sucxpdom  9268  isfinite2  9311  fin2inf  9319  fodomfir  9345  card2on  9573  djuxpdom  10205  djufi  10206  infdif  10227  cfslb2n  10287  isfin5  10318  isfin6  10319  isfin4p1  10334  fin56  10412  fin67  10414  sdomsdomcard  10579  gchi  10643  canthp1lem1  10671  canthp1lem2  10672  canthp1  10673  frgpnabl  19861  fphpd  42806  sdomne0  43404  sdomne0d  43405