|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > relsdom | Structured version Visualization version GIF version | ||
| Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.) | 
| Ref | Expression | 
|---|---|
| relsdom | ⊢ Rel ≺ | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | reldom 8992 | . 2 ⊢ Rel ≼ | |
| 2 | reldif 5824 | . . 3 ⊢ (Rel ≼ → Rel ( ≼ ∖ ≈ )) | |
| 3 | df-sdom 8989 | . . . 4 ⊢ ≺ = ( ≼ ∖ ≈ ) | |
| 4 | 3 | releqi 5786 | . . 3 ⊢ (Rel ≺ ↔ Rel ( ≼ ∖ ≈ )) | 
| 5 | 2, 4 | sylibr 234 | . 2 ⊢ (Rel ≼ → Rel ≺ ) | 
| 6 | 1, 5 | ax-mp 5 | 1 ⊢ Rel ≺ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∖ cdif 3947 Rel wrel 5689 ≈ cen 8983 ≼ cdom 8984 ≺ csdm 8985 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-dif 3953 df-ss 3967 df-opab 5205 df-xp 5690 df-rel 5691 df-dom 8988 df-sdom 8989 | 
| This theorem is referenced by: domdifsn 9095 sucdom2OLD 9123 sdom0OLD 9150 sdomirr 9155 sdomdif 9166 sucdom2 9244 0sdom1dom 9275 sdom1OLD 9280 1sdom2dom 9284 unxpdom 9290 unxpdom2 9291 sucxpdom 9292 isfinite2 9335 fin2inf 9343 fodomfir 9369 card2on 9595 djuxpdom 10227 djufi 10228 infdif 10249 cfslb2n 10309 isfin5 10340 isfin6 10341 isfin4p1 10356 fin56 10434 fin67 10436 sdomsdomcard 10601 gchi 10665 canthp1lem1 10693 canthp1lem2 10694 canthp1 10695 frgpnabl 19894 fphpd 42832 sdomne0 43431 sdomne0d 43432 | 
| Copyright terms: Public domain | W3C validator |