![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > endomtr | Structured version Visualization version GIF version |
Description: Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.) |
Ref | Expression |
---|---|
endomtr | ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | endom 8222 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) | |
2 | domtr 8248 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | |
3 | 1, 2 | sylan 576 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 class class class wbr 4843 ≈ cen 8192 ≼ cdom 8193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-f1o 6108 df-en 8196 df-dom 8197 |
This theorem is referenced by: cnvct 8272 undom 8290 xpdom1g 8299 xpdom3 8300 domunsncan 8302 domsdomtr 8337 domen1 8344 mapdom1 8367 mapdom2 8373 mapdom3 8374 php 8386 onomeneq 8392 sucdom2 8398 hartogslem1 8689 harcard 9090 infxpenlem 9122 infpwfien 9171 alephsucdom 9188 mappwen 9221 dfac12lem2 9254 cdalepw 9306 fictb 9355 cfflb 9369 canthp1lem1 9762 pwfseqlem5 9773 pwxpndom2 9775 pwcdandom 9777 gchxpidm 9779 gchhar 9789 tskinf 9879 inar1 9885 gruina 9928 rexpen 15293 mreexdomd 16624 hauspwdom 21633 rectbntr0 22963 rabfodom 29862 snct 30009 dya2iocct 30858 finminlem 32825 lindsdom 33892 poimirlem26 33924 heiborlem3 34099 pellexlem4 38182 pellexlem5 38183 mpct 40145 aacllem 43349 |
Copyright terms: Public domain | W3C validator |