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

Theorem ssdomg 8155
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 4938 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
2 simpr 471 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐵𝑉)
3 f1oi 6315 . . . . . . . . . 10 ( I ↾ 𝐴):𝐴1-1-onto𝐴
4 dff1o3 6284 . . . . . . . . . 10 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴)))
53, 4mpbi 220 . . . . . . . . 9 (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴))
65simpli 470 . . . . . . . 8 ( I ↾ 𝐴):𝐴onto𝐴
7 fof 6256 . . . . . . . 8 (( I ↾ 𝐴):𝐴onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
86, 7ax-mp 5 . . . . . . 7 ( I ↾ 𝐴):𝐴𝐴
9 fss 6196 . . . . . . 7 ((( I ↾ 𝐴):𝐴𝐴𝐴𝐵) → ( I ↾ 𝐴):𝐴𝐵)
108, 9mpan 670 . . . . . 6 (𝐴𝐵 → ( I ↾ 𝐴):𝐴𝐵)
11 funi 6063 . . . . . . . 8 Fun I
12 cnvi 5678 . . . . . . . . 9 I = I
1312funeqi 6052 . . . . . . . 8 (Fun I ↔ Fun I )
1411, 13mpbir 221 . . . . . . 7 Fun I
15 funres11 6106 . . . . . . 7 (Fun I → Fun ( I ↾ 𝐴))
1614, 15ax-mp 5 . . . . . 6 Fun ( I ↾ 𝐴)
1710, 16jctir 510 . . . . 5 (𝐴𝐵 → (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
18 df-f1 6036 . . . . 5 (( I ↾ 𝐴):𝐴1-1𝐵 ↔ (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
1917, 18sylibr 224 . . . 4 (𝐴𝐵 → ( I ↾ 𝐴):𝐴1-1𝐵)
2019adantr 466 . . 3 ((𝐴𝐵𝐵𝑉) → ( I ↾ 𝐴):𝐴1-1𝐵)
21 f1dom2g 8127 . . 3 ((𝐴 ∈ V ∧ 𝐵𝑉 ∧ ( I ↾ 𝐴):𝐴1-1𝐵) → 𝐴𝐵)
221, 2, 20, 21syl3anc 1476 . 2 ((𝐴𝐵𝐵𝑉) → 𝐴𝐵)
2322expcom 398 1 (𝐵𝑉 → (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  Vcvv 3351  wss 3723   class class class wbr 4786   I cid 5156  ccnv 5248  cres 5251  Fun wfun 6025  wf 6027  1-1wf1 6028  ontowfo 6029  1-1-ontowf1o 6030  cdom 8107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-dom 8111
This theorem is referenced by:  cnvct  8186  ssct  8197  undom  8204  xpdom3  8214  domunsncan  8216  0domg  8243  domtriord  8262  sdomel  8263  sdomdif  8264  onsdominel  8265  pwdom  8268  2pwuninel  8271  mapdom1  8281  mapdom3  8288  limenpsi  8291  php  8300  php2  8301  php3  8302  onomeneq  8306  nndomo  8310  sucdom2  8312  unbnn  8372  nnsdomg  8375  fodomfi  8395  fidomdm  8399  pwfilem  8416  hartogslem1  8603  hartogs  8605  card2on  8615  wdompwdom  8639  wdom2d  8641  wdomima2g  8647  unxpwdom2  8649  unxpwdom  8650  harwdom  8651  r1sdom  8801  tskwe  8976  carddomi2  8996  cardsdomelir  8999  cardsdomel  9000  harcard  9004  carduni  9007  cardmin2  9024  infxpenlem  9036  ssnum  9062  acnnum  9075  fodomfi2  9083  inffien  9086  alephordi  9097  dfac12lem2  9168  cdadom3  9212  cdainflem  9215  cdainf  9216  unctb  9229  infunabs  9231  infcda  9232  infdif  9233  infdif2  9234  infmap2  9242  ackbij2  9267  fictb  9269  cfslb  9290  fincssdom  9347  fin67  9419  fin1a2lem12  9435  axcclem  9481  dmct  9548  brdom3  9552  brdom5  9553  brdom4  9554  imadomg  9558  fnct  9561  mptct  9562  ondomon  9587  alephval2  9596  alephadd  9601  alephmul  9602  alephexp1  9603  alephsuc3  9604  alephexp2  9605  alephreg  9606  pwcfsdom  9607  cfpwsdom  9608  canthnum  9673  pwfseqlem5  9687  pwxpndom2  9689  pwcdandom  9691  gchaleph  9695  gchaleph2  9696  gchac  9705  winainflem  9717  gchina  9723  tsksdom  9780  tskinf  9793  inttsk  9798  inar1  9799  inatsk  9802  tskord  9804  tskcard  9805  grudomon  9841  gruina  9842  axgroth2  9849  axgroth6  9852  grothac  9854  hashun2  13374  hashss  13399  hashsslei  13415  isercoll  14606  o1fsum  14752  incexc2  14777  znnen  15147  qnnen  15148  rpnnen  15162  ruc  15178  phicl2  15680  phibnd  15683  4sqlem11  15866  vdwlem11  15902  0ram  15931  mreexdomd  16517  pgpssslw  18236  fislw  18247  cctop  21031  1stcfb  21469  2ndc1stc  21475  1stcrestlem  21476  2ndcctbss  21479  2ndcdisj2  21481  2ndcsep  21483  dis2ndc  21484  csdfil  21918  ufilen  21954  opnreen  22854  rectbntr0  22855  ovolctb2  23480  uniiccdif  23566  dyadmbl  23588  opnmblALT  23591  vitali  23601  mbfimaopnlem  23642  mbfsup  23651  fta1blem  24148  aannenlem3  24305  ppiwordi  25109  musum  25138  ppiub  25150  chpub  25166  dchrisum0re  25423  dirith2  25438  upgrex  26208  rabfodom  29682  abrexdomjm  29683  mptctf  29835  locfinreflem  30247  esumcst  30465  omsmeas  30725  sibfof  30742  subfaclefac  31496  erdszelem10  31520  snmlff  31649  finminlem  32649  phpreu  33726  lindsdom  33736  poimirlem26  33768  mblfinlem1  33779  abrexdom  33857  heiborlem3  33944  ctbnfien  37908  pellexlem4  37922  pellexlem5  37923  ttac  38129  idomodle  38300  idomsubgmo  38302  uzct  39753  smfaddlem2  41492  smfmullem4  41521  smfpimbor1lem1  41525  aacllem  43078
  Copyright terms: Public domain W3C validator