Theorem relsdom 8502

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 8501	. 2 ⊢ Rel ≼
2		reldif 5674	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8498	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5638	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 236	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

Syntax hints:   ∖ cdif 3921  Rel wrel 5546   ≈ cen 8492   ≼ cdom 8493   ≺ csdm 8494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-opab 5115  df-xp 5547  df-rel 5548  df-dom 8497  df-sdom 8498

This theorem is referenced by:  domdifsn  8586  sdom0  8635  sdomirr  8640  sdomdif  8651  sucdom2  8700  sdom1  8704  unxpdom  8711  unxpdom2  8712  sucxpdom  8713  isfinite2  8762  fin2inf  8767  card2on  9004  djuxpdom  9597  djufi  9598  infdif  9617  cfslb2n  9676  isfin5  9707  isfin6  9708  isfin4p1  9723  fin56  9801  fin67  9803  sdomsdomcard  9968  gchi  10032  canthp1lem1  10060  canthp1lem2  10061  canthp1  10062  frgpnabl  18978  fphpd  39505