Theorem relsdom 7573

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 7572	. 2 |- Rel ~<_
2		reldif 4952	. . 3 |- ( Rel ~<_ -> Rel ( ~<_ \ ~~ ) )
3		df-sdom 7569	. . . 4 |- ~< = ( ~<_ \ ~~ )
4	3	releqi 4917	. . 3 |- ( Rel ~< <-> Rel ( ~<_ \ ~~ ) )
5	2, 4	sylibr 216	. 2 |- ( Rel ~<_ -> Rel ~< )
6	1, 5	ax-mp 5	1 |- Rel ~<

Syntax hints:   \ cdif 3400   Rel wrel 4838   ~~ cen 7563   ~<_ cdom 7564   ~< csdm 7565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-xp 4839  df-rel 4840  df-dom 7568  df-sdom 7569

This theorem is referenced by:  domdifsn  7652  sdom0  7701  sdomirr  7706  sdomdif  7717  sucdom2  7765  sdom1  7769  unxpdom  7776  unxpdom2  7777  sucxpdom  7778  isfinite2  7826  fin2inf  7831  card2on  8066  cdaxpdom  8616  cdafi  8617  cfslb2n  8695  isfin5  8726  isfin6  8727  isfin4-3  8742  fin56  8820  fin67  8822  sdomsdomcard  8982  gchi  9046  canthp1lem1  9074  canthp1lem2  9075  canthp1  9076  frgpnabl  17504  fphpd  35653