Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reldom | Structured version Visualization version GIF version |
Description: Dominance is a relation. (Contributed by NM, 28-Mar-1998.) |
Ref | Expression |
---|---|
reldom | ⊢ Rel ≼ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dom 8503 | . 2 ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | |
2 | 1 | relopabi 5687 | 1 ⊢ Rel ≼ |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1774 Rel wrel 5553 –1-1→wf1 6345 ≼ cdom 8499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-opab 5120 df-xp 5554 df-rel 5555 df-dom 8503 |
This theorem is referenced by: relsdom 8508 brdomg 8511 brdomi 8512 ctex 8516 domtr 8554 undom 8597 xpdom2 8604 xpdom1g 8606 domunsncan 8609 sbth 8629 sbthcl 8631 dom0 8637 fodomr 8660 pwdom 8661 domssex 8670 mapdom1 8674 mapdom2 8680 fineqv 8725 infsdomnn 8771 infn0 8772 elharval 9019 harword 9021 domwdom 9030 unxpwdom 9045 infdifsn 9112 infdiffi 9113 ac10ct 9452 djudom2 9601 djuinf 9606 infdju1 9607 pwdjuidm 9609 djulepw 9610 infdjuabs 9620 infunabs 9621 pwdjudom 9630 infpss 9631 infmap2 9632 fictb 9659 infpssALT 9727 fin34 9804 ttukeylem1 9923 fodomb 9940 wdomac 9941 brdom3 9942 iundom2g 9954 iundom 9956 infxpidm 9976 gchdomtri 10043 pwfseq 10078 pwxpndom2 10079 pwxpndom 10080 pwdjundom 10081 gchdjuidm 10082 gchpwdom 10084 gchaclem 10092 reexALT 12375 hashdomi 13733 1stcrestlem 22052 hauspwdom 22101 ufilen 22530 ovoliunnul 24100 ovoliunnfl 34926 voliunnfl 34928 volsupnfl 34929 nnfoctb 41300 meadjiun 42739 caragenunicl 42797 |
Copyright terms: Public domain | W3C validator |