![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > endom | Structured version Visualization version GIF version |
Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.) |
Ref | Expression |
---|---|
endom | ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enssdom 8253 | . 2 ⊢ ≈ ⊆ ≼ | |
2 | 1 | ssbri 4920 | 1 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 4875 ≈ cen 8225 ≼ cdom 8226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5007 ax-nul 5015 ax-pr 5129 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 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 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-br 4876 df-opab 4938 df-xp 5352 df-rel 5353 df-f1o 6134 df-en 8229 df-dom 8230 |
This theorem is referenced by: bren2 8259 domrefg 8263 endomtr 8286 domentr 8287 domunsncan 8335 sbthb 8356 sdomentr 8369 ensdomtr 8371 domtriord 8381 domunsn 8385 xpen 8398 unxpdom2 8443 sucxpdom 8444 wdomen1 8757 wdomen2 8758 fidomtri2 9140 prdom2 9149 acnen 9196 acnen2 9198 alephdom 9224 alephinit 9238 uncdadom 9315 pwcdadom 9360 fin1a2lem11 9554 hsmexlem1 9570 gchdomtri 9773 gchcdaidm 9812 gchxpidm 9813 gchpwdom 9814 gchhar 9823 gruina 9962 nnct 13082 odinf 18338 hauspwdom 21682 ufildom1 22107 iscmet3 23468 ovolctb2 23665 mbfaddlem 23833 heiborlem3 34149 zct 40041 qct 40369 caratheodory 41530 |
Copyright terms: Public domain | W3C validator |