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 8514 | . 2 ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | |
2 | 1 | relopabi 5697 | 1 ⊢ Rel ≼ |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1779 Rel wrel 5563 –1-1→wf1 6355 ≼ cdom 8510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-opab 5132 df-xp 5564 df-rel 5565 df-dom 8514 |
This theorem is referenced by: relsdom 8519 brdomg 8522 brdomi 8523 ctex 8527 domtr 8565 undom 8608 xpdom2 8615 xpdom1g 8617 domunsncan 8620 sbth 8640 sbthcl 8642 dom0 8648 fodomr 8671 pwdom 8672 domssex 8681 mapdom1 8685 mapdom2 8691 fineqv 8736 infsdomnn 8782 infn0 8783 elharval 9030 harword 9032 domwdom 9041 unxpwdom 9056 infdifsn 9123 infdiffi 9124 ac10ct 9463 djudom2 9612 djuinf 9617 infdju1 9618 pwdjuidm 9620 djulepw 9621 infdjuabs 9631 infunabs 9632 pwdjudom 9641 infpss 9642 infmap2 9643 fictb 9670 infpssALT 9738 fin34 9815 ttukeylem1 9934 fodomb 9951 wdomac 9952 brdom3 9953 iundom2g 9965 iundom 9967 infxpidm 9987 gchdomtri 10054 pwfseq 10089 pwxpndom2 10090 pwxpndom 10091 pwdjundom 10092 gchdjuidm 10093 gchpwdom 10095 gchaclem 10103 reexALT 12386 hashdomi 13744 1stcrestlem 22063 hauspwdom 22112 ufilen 22541 ovoliunnul 24111 ovoliunnfl 34938 voliunnfl 34940 volsupnfl 34941 nnfoctb 41315 meadjiun 42755 caragenunicl 42813 |
Copyright terms: Public domain | W3C validator |