MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssdomg Unicode version

Theorem ssdomg 7265
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.)
Assertion
Ref Expression
ssdomg

Proof of Theorem ssdomg
StepHypRef Expression
1 ssexg 4448 . . 3
2 simpr 449 . . 3
3 f1oi 5670 . . . . . . . . . 10
4 dff1o3 5641 . . . . . . . . . 10
53, 4mpbi 201 . . . . . . . . 9
65simpli 446 . . . . . . . 8
7 fof 5614 . . . . . . . 8
86, 7ax-mp 5 . . . . . . 7
9 fss 5564 . . . . . . 7
108, 9mpan 653 . . . . . 6
11 funi 5447 . . . . . . . 8
12 cnvi 5242 . . . . . . . . 9
1312funeqi 5437 . . . . . . . 8
1411, 13mpbir 202 . . . . . . 7
15 funres11 5483 . . . . . . 7
1614, 15ax-mp 5 . . . . . 6
1710, 16jctir 526 . . . . 5
18 df-f1 5422 . . . . 5
1917, 18sylibr 205 . . . 4
2019adantr 453 . . 3
21 f1dom2g 7237 . . 3
221, 2, 20, 21syl3anc 1192 . 2
2322expcom 426 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  e.wcel 1724   cvv 3006  C_wss 3353   class class class wbr 4302   cid 4634  `'ccnv 4843  |`cres 4846  Funwfun 5411  -->wf 5413  -1-1->wf1 5414  -onto->wfo 5415  -1-1-onto->wf1o 5416   cdom 7219
This theorem is referenced by:  undom  7308  xpdom3  7318  domunsncan  7320  0domg  7346  domtriord  7365  sdomel  7366  sdomdif  7367  onsdominel  7368  pwdom  7371  2pwuninel  7374  mapdom1  7384  mapdom3  7391  limenpsi  7394  php  7403  php2  7404  php3  7405  onomeneq  7408  nndomo  7412  sucdom2  7415  unbnn  7475  nnsdomg  7478  fodomfi  7497  fidomdm  7500  pwfilem  7513  hartogslem1  7623  hartogs  7625  card2on  7634  wdompwdom  7658  wdom2d  7660  wdomima2g  7666  unxpwdom2  7668  unxpwdom  7669  harwdom  7670  r1sdom  7812  tskwe  7951  carddomi2  7971  cardsdomelir  7974  cardsdomel  7975  harcard  7979  carduni  7982  cardmin2  7999  infxpenlem  8009  ssnum  8034  acnnum  8047  fodomfi2  8055  inffien  8058  alephordi  8069  dfac12lem2  8138  cdadom3  8182  cdainflem  8185  cdainf  8186  unctb  8199  infunabs  8201  infcda  8202  infdif  8203  infdif2  8204  infmap2  8212  ackbij2  8237  fictb  8239  cfslb  8260  fincssdom  8317  fin67  8389  fin1a2lem12  8405  axcclem  8451  brdom3  8520  brdom5  8521  brdom4  8522  imadomg  8526  ondomon  8552  alephval2  8561  alephadd  8566  alephmul  8567  alephexp1  8568  alephsuc3  8569  alephexp2  8570  alephreg  8571  pwcfsdom  8572  cfpwsdom  8573  canthnum  8638  pwfseqlem5  8652  pwxpndom2  8654  pwcdandom  8656  gchaleph  8660  gchaleph2  8661  gchac  8670  winainflem  8682  gchina  8688  tsksdom  8745  tskinf  8758  inttsk  8763  inar1  8764  inatsk  8767  tskord  8769  tskcard  8770  grudomon  8806  gruina  8807  axgroth2  8814  axgroth6  8817  grothac  8819  hashun2  11938  hashss  11958  hashsslei  11968  isercoll  12931  o1fsum  13062  incexc2  13087  xpnnenOLD  13278  znnen  13281  qnnen  13282  rpnnen  13295  ruc  13311  phicl2  13629  phibnd  13632  4sqlem11  13802  vdwlem11  13838  0ram  13867  mreexdomd  14365  pgpssslw  15751  fislw  15762  cctop  17573  1stcfb  18012  2ndc1stc  18018  1stcrestlem  18019  2ndcctbss  18022  2ndcdisj2  18024  2ndcsep  18026  dis2ndc  18027  csdfil  18430  ufilen  18466  opnreen  19366  rectbntr0  19367  ovolctb2  19892  uniiccdif  19974  dyadmbl  19996  opnmblALT  19999  vitali  20009  mbfimaopnlem  20049  mbfsup  20058  fta1blem  20595  aannenlem3  20751  ppiwordi  21454  musum  21485  ppiub  21497  chpub  21513  dchrisum0re  21716  dirith2  21731  umgraex  21867  konigsberg  22218  abrexdomjm  24504  ssct  24630  fnct  24634  dmct  24635  cnvct  24636  mptct  24639  mptctf  24642  esumcst  25185  sibfof  25391  subfaclefac  25701  erdszelem10  25725  snmlff  25855  mblfinlem1  27099  finminlem  27184  abrexdom  27295  heiborlem3  27385  ctbnfien  27808  pellexlem4  27824  pellexlem5  27825  ttac  28036  idomodle  28418  idomsubgmo  28420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-id 4639  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-dom 7223
  Copyright terms: Public domain W3C validator