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

Theorem ssdomg 7202
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 4388 . . 3
2 simpr 449 . . 3
3 f1oi 5760 . . . . . . . . . 10
4 dff1o3 5727 . . . . . . . . . 10
53, 4mpbi 201 . . . . . . . . 9
65simpli 446 . . . . . . . 8
7 fof 5700 . . . . . . . 8
86, 7ax-mp 5 . . . . . . 7
9 fss 5646 . . . . . . 7
108, 9mpan 653 . . . . . 6
11 funi 5530 . . . . . . . 8
12 cnvi 5320 . . . . . . . . 9
1312funeqi 5521 . . . . . . . 8
1411, 13mpbir 202 . . . . . . 7
15 funres11 5568 . . . . . . 7
1614, 15ax-mp 5 . . . . . 6
1710, 16jctir 526 . . . . 5
18 df-f1 5506 . . . . 5
1917, 18sylibr 205 . . . 4
2019adantr 453 . . 3
21 f1dom2g 7174 . . 3
221, 2, 20, 21syl3anc 1185 . 2
2322expcom 426 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  e.wcel 1728   cvv 2965  C_wss 3309   class class class wbr 4243   cid 4534  `'ccnv 4918  |`cres 4921  Funwfun 5495  -->wf 5497  -1-1->wf1 5498  -onto->wfo 5499  -1-1-onto->wf1o 5500   cdom 7156
This theorem is referenced by:  undom  7245  xpdom3  7255  domunsncan  7257  0domg  7283  domtriord  7302  sdomel  7303  sdomdif  7304  onsdominel  7305  pwdom  7308  2pwuninel  7311  mapdom1  7321  mapdom3  7328  limenpsi  7331  php  7340  php2  7341  php3  7342  onomeneq  7345  nndomo  7349  sucdom2  7352  unbnn  7412  nnsdomg  7415  fodomfi  7434  fidomdm  7437  pwfilem  7450  hartogslem1  7560  hartogs  7562  card2on  7571  wdompwdom  7595  wdom2d  7597  wdomima2g  7603  unxpwdom2  7605  unxpwdom  7606  harwdom  7607  r1sdom  7749  tskwe  7888  carddomi2  7908  cardsdomelir  7911  cardsdomel  7912  harcard  7916  carduni  7919  cardmin2  7936  infxpenlem  7946  ssnum  7971  acnnum  7984  fodomfi2  7992  inffien  7995  alephordi  8006  dfac12lem2  8075  cdadom3  8119  cdainflem  8122  cdainf  8123  unctb  8136  infunabs  8138  infcda  8139  infdif  8140  infdif2  8141  infmap2  8149  ackbij2  8174  fictb  8176  cfslb  8197  fincssdom  8254  fin67  8326  fin1a2lem12  8342  axcclem  8388  brdom3  8457  brdom5  8458  brdom4  8459  imadomg  8463  ondomon  8489  alephval2  8498  alephadd  8503  alephmul  8504  alephexp1  8505  alephsuc3  8506  alephexp2  8507  alephreg  8508  pwcfsdom  8509  cfpwsdom  8510  canthnum  8575  pwfseqlem5  8589  pwxpndom2  8591  pwcdandom  8593  gchaleph  8597  gchaleph2  8598  gchac  8607  winainflem  8619  gchina  8625  tsksdom  8682  tskinf  8695  inttsk  8700  inar1  8701  inatsk  8704  tskord  8706  tskcard  8707  grudomon  8743  gruina  8744  axgroth2  8751  axgroth6  8754  grothac  8756  hashun2  11708  hashsslei  11736  isercoll  12512  o1fsum  12643  incexc2  12669  xpnnenOLD  12860  znnen  12863  qnnen  12864  rpnnen  12877  ruc  12893  phicl2  13208  phibnd  13211  4sqlem11  13374  vdwlem11  13410  0ram  13439  mreexdomd  13925  pgpssslw  15299  fislw  15310  cctop  17121  1stcfb  17559  2ndc1stc  17565  1stcrestlem  17566  2ndcctbss  17569  2ndcdisj2  17571  2ndcsep  17573  dis2ndc  17574  csdfil  17977  ufilen  18013  opnreen  18913  rectbntr0  18914  ovolctb2  19439  uniiccdif  19521  dyadmbl  19543  opnmblALT  19546  vitali  19556  mbfimaopnlem  19596  mbfsup  19605  fta1blem  20142  aannenlem3  20298  ppiwordi  20996  musum  21027  ppiub  21039  chpub  21055  dchrisum0re  21258  dirith2  21273  umgraex  21409  konigsberg  21760  abrexdomjm  24037  ssct  24149  fnct  24153  dmct  24154  cnvct  24155  mptct  24157  mptctf  24160  esumcst  24504  sibfof  24703  subfaclefac  24966  erdszelem10  24990  snmlff  25120  mblfinlem1  26352  finminlem  26432  abrexdom  26543  heiborlem3  26633  ctbnfien  27058  pellexlem4  27074  pellexlem5  27075  ttac  27286  idomodle  27668  idomsubgmo  27670  hashss  28356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pow 4416  ax-pr 4442  ax-un 4742
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3766  df-pw 3828  df-sn 3847  df-pr 3848  df-op 3850  df-uni 4044  df-br 4244  df-opab 4302  df-id 4539  df-xp 4925  df-rel 4926  df-cnv 4927  df-co 4928  df-dm 4929  df-rn 4930  df-res 4931  df-ima 4932  df-fun 5503  df-fn 5504  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508  df-dom 7160
  Copyright terms: Public domain W3C validator