| 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 8987 | . 2 ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | |
| 2 | 1 | relopabiv 5830 | 1 ⊢ Rel ≼ |
| Colors of variables: wff setvar class |
| Syntax hints: ∃wex 1779 Rel wrel 5690 –1-1→wf1 6558 ≼ cdom 8983 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 df-dom 8987 |
| This theorem is referenced by: relsdom 8992 brdomg 8997 brdomgOLD 8998 brdomi 8999 brdomiOLD 9000 ctex 9004 domssl 9038 domssr 9039 domtr 9047 undom 9099 undomOLD 9100 xpdom2 9107 xpdom1g 9109 domunsncan 9112 sbth 9133 sbthcl 9135 dom0OLD 9143 fodomr 9168 pwdom 9169 domssex 9178 mapdom1 9182 mapdom2 9188 domtrfil 9232 sbthfi 9239 0sdom1dom 9274 1sdom2dom 9283 fineqv 9299 infsdomnn 9338 infsdomnnOLD 9339 infn0ALT 9341 elharval 9601 harword 9603 domwdom 9614 unxpwdom 9629 infdifsn 9697 infdiffi 9698 ac10ct 10074 djudom2 10224 djuinf 10229 infdju1 10230 pwdjuidm 10232 djulepw 10233 infdjuabs 10245 infunabs 10246 pwdjudom 10255 infpss 10256 infmap2 10257 fictb 10284 infpssALT 10353 fin34 10430 ttukeylem1 10549 fodomb 10566 wdomac 10567 brdom3 10568 iundom2g 10580 iundom 10582 infxpidm 10602 gchdomtri 10669 pwfseq 10704 pwxpndom2 10705 pwxpndom 10706 pwdjundom 10707 gchdjuidm 10708 gchpwdom 10710 gchaclem 10718 reexALT 13026 hashdomi 14419 1stcrestlem 23460 hauspwdom 23509 ufilen 23938 ovoliunnul 25542 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 nnfoctb 45053 rn1st 45280 meadjiun 46481 caragenunicl 46539 |
| Copyright terms: Public domain | W3C validator |