Theorem relsdom 7513

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 7512	. 2 |- Rel ~<_
2		reldif 5113	. . 3 |- ( Rel ~<_ -> Rel ( ~<_ \ ~~ ) )
3		df-sdom 7509	. . . 4 |- ~< = ( ~<_ \ ~~ )
4	3	releqi 5077	. . 3 |- ( Rel ~< <-> Rel ( ~<_ \ ~~ ) )
5	2, 4	sylibr 212	. 2 |- ( Rel ~<_ -> Rel ~< )
6	1, 5	ax-mp 5	1 |- Rel ~<

Syntax hints:   \ cdif 3466   Rel wrel 4997   ~~ cen 7503   ~<_ cdom 7504   ~< csdm 7505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-opab 4499  df-xp 4998  df-rel 4999  df-dom 7508  df-sdom 7509

This theorem is referenced by:  domdifsn  7590  sdom0  7639  sdomirr  7644  sdomdif  7655  sucdom2  7704  sdom1  7709  unxpdom  7717  unxpdom2  7718  sucxpdom  7719  isfinite2  7767  fin2inf  7772  card2on  7969  cdaxpdom  8558  cdafi  8559  cfslb2n  8637  isfin5  8668  isfin6  8669  isfin4-3  8684  fin56  8762  fin67  8764  sdomsdomcard  8924  gchi  8991  canthp1lem1  9019  canthp1lem2  9020  canthp1  9021  frgpnabl  16663  fphpd  30341