![]() |
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 8224 | . 2 ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | |
2 | 1 | relopabi 5478 | 1 ⊢ Rel ≼ |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1880 Rel wrel 5347 –1-1→wf1 6120 ≼ cdom 8220 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-opab 4936 df-xp 5348 df-rel 5349 df-dom 8224 |
This theorem is referenced by: relsdom 8229 brdomg 8232 brdomi 8233 ctex 8237 domtr 8275 undom 8317 xpdom2 8324 xpdom1g 8326 domunsncan 8329 sbth 8349 sbthcl 8351 dom0 8357 fodomr 8380 pwdom 8381 domssex 8390 mapdom1 8394 mapdom2 8400 fineqv 8444 infsdomnn 8490 infn0 8491 elharval 8737 harword 8739 domwdom 8748 unxpwdom 8763 infdifsn 8831 infdiffi 8832 ac10ct 9170 iunfictbso 9250 cdadom1 9323 cdainf 9329 infcda1 9330 pwcdaidm 9332 cdalepw 9333 unctb 9342 infcdaabs 9343 infunabs 9344 infpss 9354 infmap2 9355 fictb 9382 infpssALT 9450 fin34 9527 ttukeylem1 9646 fodomb 9663 wdomac 9664 brdom3 9665 iundom2g 9677 iundom 9679 infxpidm 9699 iunctb 9711 gchdomtri 9766 pwfseq 9801 pwxpndom2 9802 pwxpndom 9803 pwcdandom 9804 gchpwdom 9807 gchaclem 9815 reexALT 12106 hashdomi 13459 1stcrestlem 21626 2ndcdisj2 21631 dis2ndc 21634 hauspwdom 21675 ufilen 22104 ovoliunnul 23673 uniiccdif 23744 ovoliunnfl 33995 voliunnfl 33997 volsupnfl 33998 nnfoctb 40030 meadjiun 41474 caragenunicl 41532 |
Copyright terms: Public domain | W3C validator |