![]() |
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 8947 | . 2 ⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | |
2 | 1 | relopabiv 5820 | 1 ⊢ Rel ≼ |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1780 Rel wrel 5681 –1-1→wf1 6540 ≼ cdom 8943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 df-opab 5211 df-xp 5682 df-rel 5683 df-dom 8947 |
This theorem is referenced by: relsdom 8952 brdomg 8958 brdomgOLD 8959 brdomi 8960 brdomiOLD 8961 ctex 8965 domssl 9000 domssr 9001 domtr 9009 undom 9065 undomOLD 9066 xpdom2 9073 xpdom1g 9075 domunsncan 9078 sbth 9099 sbthcl 9101 dom0OLD 9109 fodomr 9134 pwdom 9135 domssex 9144 mapdom1 9148 mapdom2 9154 domtrfil 9201 sbthfi 9208 0sdom1dom 9244 1sdom2dom 9253 fineqv 9269 infsdomnn 9311 infsdomnnOLD 9312 infn0ALT 9314 elharval 9562 harword 9564 domwdom 9575 unxpwdom 9590 infdifsn 9658 infdiffi 9659 ac10ct 10035 djudom2 10184 djuinf 10189 infdju1 10190 pwdjuidm 10192 djulepw 10193 infdjuabs 10207 infunabs 10208 pwdjudom 10217 infpss 10218 infmap2 10219 fictb 10246 infpssALT 10314 fin34 10391 ttukeylem1 10510 fodomb 10527 wdomac 10528 brdom3 10529 iundom2g 10541 iundom 10543 infxpidm 10563 gchdomtri 10630 pwfseq 10665 pwxpndom2 10666 pwxpndom 10667 pwdjundom 10668 gchdjuidm 10669 gchpwdom 10671 gchaclem 10679 reexALT 12975 hashdomi 14347 1stcrestlem 23276 hauspwdom 23325 ufilen 23754 ovoliunnul 25356 ovoliunnfl 36994 voliunnfl 36996 volsupnfl 36997 nnfoctb 44196 rn1st 44437 meadjiun 45641 caragenunicl 45699 |
Copyright terms: Public domain | W3C validator |