![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relsdom | Structured version Visualization version Unicode version |
Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.) |
Ref | Expression |
---|---|
relsdom |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldom 7572 |
. 2
![]() ![]() ![]() | |
2 | reldif 4952 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-sdom 7569 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | releqi 4917 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | sylibr 216 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | ax-mp 5 |
1
![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |