![]() |
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 8915 | . 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶) | |
2 | domtr 8943 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | |
3 | 1, 2 | sylan2 593 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 class class class wbr 5103 ≈ cen 8876 ≼ cdom 8877 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7668 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-f1o 6500 df-en 8880 df-dom 8881 |
This theorem is referenced by: domdifsn 8994 xpdom1g 9009 domunsncan 9012 sdomdomtr 9050 domen2 9060 mapdom2 9088 phpOLD 9162 unxpdom2 9194 sucxpdom 9195 xpfir 9206 fodomfi 9265 cardsdomelir 9905 infxpenlem 9945 xpct 9948 infpwfien 9994 inffien 9995 mappwen 10044 iunfictbso 10046 djuxpdom 10117 cdainflem 10119 djuinf 10120 djulepw 10124 ficardun2 10134 ficardun2OLD 10135 unctb 10137 infdjuabs 10138 infunabs 10139 infdju 10140 infdif 10141 infxpdom 10143 pwdjudom 10148 infmap2 10150 fictb 10177 cfslb 10198 fin1a2lem11 10342 fnct 10469 unirnfdomd 10499 iunctb 10506 alephreg 10514 cfpwsdom 10516 gchdomtri 10561 canthp1lem1 10584 pwfseqlem5 10595 pwxpndom 10598 gchdjuidm 10600 gchxpidm 10601 gchpwdom 10602 gchhar 10611 inttsk 10706 inar1 10707 tskcard 10713 znnen 16086 qnnen 16087 rpnnen 16101 rexpen 16102 aleph1irr 16120 cygctb 19660 1stcfb 22780 2ndcredom 22785 2ndcctbss 22790 hauspwdom 22836 tx2ndc 22986 met1stc 23861 met2ndci 23862 re2ndc 24148 opnreen 24178 ovolctb2 24840 ovolfi 24842 uniiccdif 24926 dyadmbl 24948 opnmblALT 24951 vitali 24961 mbfimaopnlem 25003 mbfsup 25012 aannenlem3 25674 dmvlsiga 32597 sigapildsys 32630 omssubadd 32769 carsgclctunlem3 32789 finminlem 34757 phpreu 36029 lindsdom 36039 mblfinlem1 36082 pellexlem4 41093 pellexlem5 41094 pr2dom 41741 tr3dom 41742 nnfoctb 43197 ioonct 43707 subsaliuncl 44531 caragenunicl 44697 aacllem 47180 |
Copyright terms: Public domain | W3C validator |