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

Theorem ssdomg 7317
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 4464 . . 3
2 simpr 449 . . 3
3 f1oi 5693 . . . . . . . . . 10
4 dff1o3 5664 . . . . . . . . . 10
53, 4mpbi 201 . . . . . . . . 9
65simpli 446 . . . . . . . 8
7 fof 5637 . . . . . . . 8
86, 7ax-mp 5 . . . . . . 7
9 fss 5585 . . . . . . 7
108, 9mpan 653 . . . . . 6
11 funi 5468 . . . . . . . 8
12 cnvi 5263 . . . . . . . . 9
1312funeqi 5458 . . . . . . . 8
1411, 13mpbir 202 . . . . . . 7
15 funres11 5504 . . . . . . 7
1614, 15ax-mp 5 . . . . . 6
1710, 16jctir 526 . . . . 5
18 df-f1 5443 . . . . 5
1917, 18sylibr 205 . . . 4
2019adantr 453 . . 3
21 f1dom2g 7289 . . 3
221, 2, 20, 21syl3anc 1192 . 2
2322expcom 426 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  e.wcel 1732   cvv 3015  C_wss 3365   class class class wbr 4318   cid 4652  `'ccnv 4861  |`cres 4864  Funwfun 5432  -->wf 5434  -1-1->wf1 5435  -onto->wfo 5436  -1-1-onto->wf1o 5437   cdom 7271
This theorem is referenced by:  undom  7361  xpdom3  7371  domunsncan  7373  0domg  7399  domtriord  7418  sdomel  7419  sdomdif  7420  onsdominel  7421  pwdom  7424  2pwuninel  7427  mapdom1  7437  mapdom3  7444  limenpsi  7447  php  7456  php2  7457  php3  7458  onomeneq  7461  nndomo  7465  sucdom2  7468  unbnn  7529  nnsdomg  7532  fodomfi  7551  fidomdm  7554  pwfilem  7567  hartogslem1  7678  hartogs  7680  card2on  7689  wdompwdom  7713  wdom2d  7715  wdomima2g  7721  unxpwdom2  7723  unxpwdom  7724  harwdom  7725  r1sdom  7867  tskwe  8006  carddomi2  8026  cardsdomelir  8029  cardsdomel  8030  harcard  8034  carduni  8037  cardmin2  8054  infxpenlem  8066  ssnum  8091  acnnum  8104  fodomfi2  8112  inffien  8115  alephordi  8126  dfac12lem2  8195  cdadom3  8239  cdainflem  8242  cdainf  8243  unctb  8256  infunabs  8258  infcda  8259  infdif  8260  infdif2  8261  infmap2  8269  ackbij2  8294  fictb  8296  cfslb  8317  fincssdom  8374  fin67  8446  fin1a2lem12  8462  axcclem  8508  brdom3  8577  brdom5  8578  brdom4  8579  imadomg  8583  ondomon  8609  alephval2  8618  alephadd  8623  alephmul  8624  alephexp1  8625  alephsuc3  8626  alephexp2  8627  alephreg  8628  pwcfsdom  8629  cfpwsdom  8630  canthnum  8695  pwfseqlem5  8709  pwxpndom2  8711  pwcdandom  8713  gchaleph  8717  gchaleph2  8718  gchac  8727  winainflem  8739  gchina  8745  tsksdom  8802  tskinf  8815  inttsk  8820  inar1  8821  inatsk  8824  tskord  8826  tskcard  8827  grudomon  8863  gruina  8864  axgroth2  8871  axgroth6  8874  grothac  8876  hashun2  11995  hashss  12015  hashsslei  12025  isercoll  12992  o1fsum  13123  incexc2  13148  xpnnenOLD  13339  znnen  13342  qnnen  13343  rpnnen  13356  ruc  13372  phicl2  13690  phibnd  13693  4sqlem11  13863  vdwlem11  13899  0ram  13928  mreexdomd  14428  pgpssslw  15857  fislw  15868  cctop  18084  1stcfb  18523  2ndc1stc  18529  1stcrestlem  18530  2ndcctbss  18533  2ndcdisj2  18535  2ndcsep  18537  dis2ndc  18538  csdfil  18941  ufilen  18977  opnreen  19877  rectbntr0  19878  ovolctb2  20403  uniiccdif  20485  dyadmbl  20507  opnmblALT  20510  vitali  20520  mbfimaopnlem  20560  mbfsup  20569  fta1blem  21106  aannenlem3  21262  ppiwordi  21966  musum  21997  ppiub  22009  chpub  22025  dchrisum0re  22228  dirith2  22243  umgraex  22379  konigsberg  22730  abrexdomjm  25016  ssct  25139  fnct  25143  dmct  25144  cnvct  25145  mptct  25148  mptctf  25151  esumcst  25694  sibfof  25900  subfaclefac  26210  erdszelem10  26234  snmlff  26364  mblfinlem1  27608  finminlem  27693  abrexdom  27804  heiborlem3  27894  ctbnfien  28305  pellexlem4  28321  pellexlem5  28322  ttac  28533  idomodle  28743  idomsubgmo  28745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-dom 7275
  Copyright terms: Public domain W3C validator