Theorem relsdom 8994

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 8993	. 2 ⊢ Rel ≼
2		reldif 5798	. . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ ))
3		df-sdom 8990	. . . 4 ⊢ ≺ = ( ≼ ∖ ≈ )
4	3	releqi 5759	. . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ ))
5	2, 4	sylibr 237	. 2 ⊢ (Rel ≼ → Rel ≺ )
6	1, 5	ax-mp 5	1 ⊢ Rel ≺

This proof depends on syntax axioms:   ∖ cdif 4048  Rel wrel 5660   ≈ cen 8984   ≼ cdom 8985   ≺ csdm 8986

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050  df-opab 5171  df-xp 5661  df-rel 5662  df-dom 8989  df-sdom 8990

This theorem is used by:  domdifsn  9093  sdomirr  9147  sdomdif  9158  sucdom2  9232  0sdom1dom  9251  1sdom2dom  9259  unxpdom  9264  unxpdom2  9265  sucxpdom  9266  isfinite2  9304  fin2inf  9310  fodomfir  9333  card2on  9561  djuxpdom  10277  djufi  10278  infdif  10299  cfslb2n  10359  isfin5  10390  isfin6  10391  isfin4p1  10406  fin56  10484  fin67  10486  sdomsdomcard  10657  gchi  10722  canthp1lem1  10750  canthp1lem2  10751  canthp1  10752  frgpnabl  20104  kardsdom  35904  fphpd  43969  sdomne0  44560  sdomne0d  44561