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

Theorem ssdomg 7581
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 4598 . . 3
2 simpr 461 . . 3
3 f1oi 5856 . . . . . . . . . 10
4 dff1o3 5827 . . . . . . . . . 10
53, 4mpbi 208 . . . . . . . . 9
65simpli 458 . . . . . . . 8
7 fof 5800 . . . . . . . 8
86, 7ax-mp 5 . . . . . . 7
9 fss 5744 . . . . . . 7
108, 9mpan 670 . . . . . 6
11 funi 5623 . . . . . . . 8
12 cnvi 5415 . . . . . . . . 9
1312funeqi 5613 . . . . . . . 8
1411, 13mpbir 209 . . . . . . 7
15 funres11 5661 . . . . . . 7
1614, 15ax-mp 5 . . . . . 6
1710, 16jctir 538 . . . . 5
18 df-f1 5598 . . . . 5
1917, 18sylibr 212 . . . 4
2019adantr 465 . . 3
21 f1dom2g 7553 . . 3
221, 2, 20, 21syl3anc 1228 . 2
2322expcom 435 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   cvv 3109  C_wss 3475   class class class wbr 4452   cid 4795  `'ccnv 5003  |`cres 5006  Funwfun 5587  -->wf 5589  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592   cdom 7534
This theorem is referenced by:  undom  7625  xpdom3  7635  domunsncan  7637  0domg  7664  domtriord  7683  sdomel  7684  sdomdif  7685  onsdominel  7686  pwdom  7689  2pwuninel  7692  mapdom1  7702  mapdom3  7709  limenpsi  7712  php  7721  php2  7722  php3  7723  onomeneq  7727  nndomo  7731  sucdom2  7734  unbnn  7796  nnsdomg  7799  fodomfi  7819  fidomdm  7822  pwfilem  7834  hartogslem1  7988  hartogs  7990  card2on  8001  wdompwdom  8025  wdom2d  8027  wdomima2g  8033  unxpwdom2  8035  unxpwdom  8036  harwdom  8037  r1sdom  8213  tskwe  8352  carddomi2  8372  cardsdomelir  8375  cardsdomel  8376  harcard  8380  carduni  8383  cardmin2  8400  infxpenlem  8412  ssnum  8441  acnnum  8454  fodomfi2  8462  inffien  8465  alephordi  8476  dfac12lem2  8545  cdadom3  8589  cdainflem  8592  cdainf  8593  unctb  8606  infunabs  8608  infcda  8609  infdif  8610  infdif2  8611  infmap2  8619  ackbij2  8644  fictb  8646  cfslb  8667  fincssdom  8724  fin67  8796  fin1a2lem12  8812  axcclem  8858  brdom3  8927  brdom5  8928  brdom4  8929  imadomg  8933  ondomon  8959  alephval2  8968  alephadd  8973  alephmul  8974  alephexp1  8975  alephsuc3  8976  alephexp2  8977  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  canthnum  9048  pwfseqlem5  9062  pwxpndom2  9064  pwcdandom  9066  gchaleph  9070  gchaleph2  9071  gchac  9080  winainflem  9092  gchina  9098  tsksdom  9155  tskinf  9168  inttsk  9173  inar1  9174  inatsk  9177  tskord  9179  tskcard  9180  grudomon  9216  gruina  9217  axgroth2  9224  axgroth6  9227  grothac  9229  hashun2  12451  hashss  12474  hashsslei  12484  isercoll  13490  o1fsum  13627  incexc2  13650  xpnnenOLD  13943  znnen  13946  qnnen  13947  rpnnen  13960  ruc  13976  phicl2  14298  phibnd  14301  4sqlem11  14473  vdwlem11  14509  0ram  14538  mreexdomd  15046  pgpssslw  16634  fislw  16645  cctop  19507  1stcfb  19946  2ndc1stc  19952  1stcrestlem  19953  2ndcctbss  19956  2ndcdisj2  19958  2ndcsep  19960  dis2ndc  19961  csdfil  20395  ufilen  20431  opnreen  21336  rectbntr0  21337  ovolctb2  21903  uniiccdif  21987  dyadmbl  22009  opnmblALT  22012  vitali  22022  mbfimaopnlem  22062  mbfsup  22071  fta1blem  22569  aannenlem3  22726  ppiwordi  23436  musum  23467  ppiub  23479  chpub  23495  dchrisum0re  23698  dirith2  23713  umgraex  24323  konigsberg  24987  rabfodom  27404  abrexdomjm  27405  ssct  27532  fnct  27536  dmct  27537  cnvct  27538  mptct  27541  mptctf  27544  locfinreflem  27843  esumcst  28071  sibfof  28282  subfaclefac  28620  erdszelem10  28644  snmlff  28774  mblfinlem1  30051  finminlem  30136  abrexdom  30221  heiborlem3  30309  ctbnfien  30752  pellexlem4  30768  pellexlem5  30769  ttac  30978  idomodle  31153  idomsubgmo  31155  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-dom 7538
  Copyright terms: Public domain W3C validator