Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > domentr | Structured version Visualization version GIF version |
Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.) |
Ref | Expression |
---|---|
domentr | ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | endom 8536 | . 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶) | |
2 | domtr 8562 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | |
3 | 1, 2 | sylan2 594 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 class class class wbr 5066 ≈ cen 8506 ≼ cdom 8507 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-f1o 6362 df-en 8510 df-dom 8511 |
This theorem is referenced by: domdifsn 8600 xpdom1g 8614 domunsncan 8617 sdomdomtr 8650 domen2 8660 mapdom2 8688 php 8701 unxpdom2 8726 sucxpdom 8727 xpfir 8740 fodomfi 8797 cardsdomelir 9402 infxpenlem 9439 xpct 9442 infpwfien 9488 inffien 9489 mappwen 9538 iunfictbso 9540 djuxpdom 9611 cdainflem 9613 djuinf 9614 djulepw 9618 ficardun2 9625 unctb 9627 infdjuabs 9628 infunabs 9629 infdju 9630 infdif 9631 infxpdom 9633 pwdjudom 9638 infmap2 9640 fictb 9667 cfslb 9688 fin1a2lem11 9832 fnct 9959 unirnfdomd 9989 iunctb 9996 alephreg 10004 cfpwsdom 10006 gchdomtri 10051 canthp1lem1 10074 pwfseqlem5 10085 pwxpndom 10088 gchdjuidm 10090 gchxpidm 10091 gchpwdom 10092 gchhar 10101 inttsk 10196 inar1 10197 tskcard 10203 znnen 15565 qnnen 15566 rpnnen 15580 rexpen 15581 aleph1irr 15599 cygctb 19012 1stcfb 22053 2ndcredom 22058 2ndcctbss 22063 hauspwdom 22109 tx2ndc 22259 met1stc 23131 met2ndci 23132 re2ndc 23409 opnreen 23439 ovolctb2 24093 ovolfi 24095 uniiccdif 24179 dyadmbl 24201 opnmblALT 24204 vitali 24214 mbfimaopnlem 24256 mbfsup 24265 aannenlem3 24919 dmvlsiga 31388 sigapildsys 31421 omssubadd 31558 carsgclctunlem3 31578 finminlem 33666 phpreu 34891 lindsdom 34901 mblfinlem1 34944 pellexlem4 39449 pellexlem5 39450 pr2dom 39913 tr3dom 39914 nnfoctb 41329 ioonct 41833 subsaliuncl 42661 caragenunicl 42826 aacllem 44922 |
Copyright terms: Public domain | W3C validator |