Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssdomg | Structured version Visualization version Unicode version |
Description: A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Ref | Expression |
---|---|
ssdomg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexg 4804 | . . 3 | |
2 | simpr 477 | . . 3 | |
3 | f1oi 6174 | . . . . . . . . . 10 | |
4 | dff1o3 6143 | . . . . . . . . . 10 | |
5 | 3, 4 | mpbi 220 | . . . . . . . . 9 |
6 | 5 | simpli 474 | . . . . . . . 8 |
7 | fof 6115 | . . . . . . . 8 | |
8 | 6, 7 | ax-mp 5 | . . . . . . 7 |
9 | fss 6056 | . . . . . . 7 | |
10 | 8, 9 | mpan 706 | . . . . . 6 |
11 | funi 5920 | . . . . . . . 8 | |
12 | cnvi 5537 | . . . . . . . . 9 | |
13 | 12 | funeqi 5909 | . . . . . . . 8 |
14 | 11, 13 | mpbir 221 | . . . . . . 7 |
15 | funres11 5966 | . . . . . . 7 | |
16 | 14, 15 | ax-mp 5 | . . . . . 6 |
17 | 10, 16 | jctir 561 | . . . . 5 |
18 | df-f1 5893 | . . . . 5 | |
19 | 17, 18 | sylibr 224 | . . . 4 |
20 | 19 | adantr 481 | . . 3 |
21 | f1dom2g 7973 | . . 3 | |
22 | 1, 2, 20, 21 | syl3anc 1326 | . 2 |
23 | 22 | expcom 451 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wcel 1990 cvv 3200 wss 3574 class class class wbr 4653 cid 5023 ccnv 5113 cres 5116 wfun 5882 wf 5884 wf1 5885 wfo 5886 wf1o 5887 cdom 7953 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-dom 7957 |
This theorem is referenced by: cnvct 8033 ssct 8041 undom 8048 xpdom3 8058 domunsncan 8060 0domg 8087 domtriord 8106 sdomel 8107 sdomdif 8108 onsdominel 8109 pwdom 8112 2pwuninel 8115 mapdom1 8125 mapdom3 8132 limenpsi 8135 php 8144 php2 8145 php3 8146 onomeneq 8150 nndomo 8154 sucdom2 8156 unbnn 8216 nnsdomg 8219 fodomfi 8239 fidomdm 8243 pwfilem 8260 hartogslem1 8447 hartogs 8449 card2on 8459 wdompwdom 8483 wdom2d 8485 wdomima2g 8491 unxpwdom2 8493 unxpwdom 8494 harwdom 8495 r1sdom 8637 tskwe 8776 carddomi2 8796 cardsdomelir 8799 cardsdomel 8800 harcard 8804 carduni 8807 cardmin2 8824 infxpenlem 8836 ssnum 8862 acnnum 8875 fodomfi2 8883 inffien 8886 alephordi 8897 dfac12lem2 8966 cdadom3 9010 cdainflem 9013 cdainf 9014 unctb 9027 infunabs 9029 infcda 9030 infdif 9031 infdif2 9032 infmap2 9040 ackbij2 9065 fictb 9067 cfslb 9088 fincssdom 9145 fin67 9217 fin1a2lem12 9233 axcclem 9279 dmct 9346 brdom3 9350 brdom5 9351 brdom4 9352 imadomg 9356 fnct 9359 mptct 9360 ondomon 9385 alephval2 9394 alephadd 9399 alephmul 9400 alephexp1 9401 alephsuc3 9402 alephexp2 9403 alephreg 9404 pwcfsdom 9405 cfpwsdom 9406 canthnum 9471 pwfseqlem5 9485 pwxpndom2 9487 pwcdandom 9489 gchaleph 9493 gchaleph2 9494 gchac 9503 winainflem 9515 gchina 9521 tsksdom 9578 tskinf 9591 inttsk 9596 inar1 9597 inatsk 9600 tskord 9602 tskcard 9603 grudomon 9639 gruina 9640 axgroth2 9647 axgroth6 9650 grothac 9652 hashun2 13172 hashss 13197 hashsslei 13213 isercoll 14398 o1fsum 14545 incexc2 14570 znnen 14941 qnnen 14942 rpnnen 14956 ruc 14972 phicl2 15473 phibnd 15476 4sqlem11 15659 vdwlem11 15695 0ram 15724 mreexdomd 16310 pgpssslw 18029 fislw 18040 cctop 20810 1stcfb 21248 2ndc1stc 21254 1stcrestlem 21255 2ndcctbss 21258 2ndcdisj2 21260 2ndcsep 21262 dis2ndc 21263 csdfil 21698 ufilen 21734 opnreen 22634 rectbntr0 22635 ovolctb2 23260 uniiccdif 23346 dyadmbl 23368 opnmblALT 23371 vitali 23382 mbfimaopnlem 23422 mbfsup 23431 fta1blem 23928 aannenlem3 24085 ppiwordi 24888 musum 24917 ppiub 24929 chpub 24945 dchrisum0re 25202 dirith2 25217 upgrex 25987 rabfodom 29344 abrexdomjm 29345 mptctf 29495 locfinreflem 29907 esumcst 30125 omsmeas 30385 sibfof 30402 subfaclefac 31158 erdszelem10 31182 snmlff 31311 finminlem 32312 phpreu 33393 lindsdom 33403 poimirlem26 33435 mblfinlem1 33446 abrexdom 33525 heiborlem3 33612 ctbnfien 37382 pellexlem4 37396 pellexlem5 37397 ttac 37603 idomodle 37774 idomsubgmo 37776 uzct 39232 smfaddlem2 40972 smfmullem4 41001 smfpimbor1lem1 41005 aacllem 42547 |
Copyright terms: Public domain | W3C validator |