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

Theorem ssdomg 8043
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 4837 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
2 simpr 476 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐵𝑉)
3 f1oi 6212 . . . . . . . . . 10 ( I ↾ 𝐴):𝐴1-1-onto𝐴
4 dff1o3 6181 . . . . . . . . . 10 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴)))
53, 4mpbi 220 . . . . . . . . 9 (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴))
65simpli 473 . . . . . . . 8 ( I ↾ 𝐴):𝐴onto𝐴
7 fof 6153 . . . . . . . 8 (( I ↾ 𝐴):𝐴onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
86, 7ax-mp 5 . . . . . . 7 ( I ↾ 𝐴):𝐴𝐴
9 fss 6094 . . . . . . 7 ((( I ↾ 𝐴):𝐴𝐴𝐴𝐵) → ( I ↾ 𝐴):𝐴𝐵)
108, 9mpan 706 . . . . . 6 (𝐴𝐵 → ( I ↾ 𝐴):𝐴𝐵)
11 funi 5958 . . . . . . . 8 Fun I
12 cnvi 5572 . . . . . . . . 9 I = I
1312funeqi 5947 . . . . . . . 8 (Fun I ↔ Fun I )
1411, 13mpbir 221 . . . . . . 7 Fun I
15 funres11 6004 . . . . . . 7 (Fun I → Fun ( I ↾ 𝐴))
1614, 15ax-mp 5 . . . . . 6 Fun ( I ↾ 𝐴)
1710, 16jctir 560 . . . . 5 (𝐴𝐵 → (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
18 df-f1 5931 . . . . 5 (( I ↾ 𝐴):𝐴1-1𝐵 ↔ (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
1917, 18sylibr 224 . . . 4 (𝐴𝐵 → ( I ↾ 𝐴):𝐴1-1𝐵)
2019adantr 480 . . 3 ((𝐴𝐵𝐵𝑉) → ( I ↾ 𝐴):𝐴1-1𝐵)
21 f1dom2g 8015 . . 3 ((𝐴 ∈ V ∧ 𝐵𝑉 ∧ ( I ↾ 𝐴):𝐴1-1𝐵) → 𝐴𝐵)
221, 2, 20, 21syl3anc 1366 . 2 ((𝐴𝐵𝐵𝑉) → 𝐴𝐵)
2322expcom 450 1 (𝐵𝑉 → (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  Vcvv 3231  wss 3607   class class class wbr 4685   I cid 5052  ccnv 5142  cres 5145  Fun wfun 5920  wf 5922  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cdom 7995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-dom 7999
This theorem is referenced by:  cnvct  8074  ssct  8082  undom  8089  xpdom3  8099  domunsncan  8101  0domg  8128  domtriord  8147  sdomel  8148  sdomdif  8149  onsdominel  8150  pwdom  8153  2pwuninel  8156  mapdom1  8166  mapdom3  8173  limenpsi  8176  php  8185  php2  8186  php3  8187  onomeneq  8191  nndomo  8195  sucdom2  8197  unbnn  8257  nnsdomg  8260  fodomfi  8280  fidomdm  8284  pwfilem  8301  hartogslem1  8488  hartogs  8490  card2on  8500  wdompwdom  8524  wdom2d  8526  wdomima2g  8532  unxpwdom2  8534  unxpwdom  8535  harwdom  8536  r1sdom  8675  tskwe  8814  carddomi2  8834  cardsdomelir  8837  cardsdomel  8838  harcard  8842  carduni  8845  cardmin2  8862  infxpenlem  8874  ssnum  8900  acnnum  8913  fodomfi2  8921  inffien  8924  alephordi  8935  dfac12lem2  9004  cdadom3  9048  cdainflem  9051  cdainf  9052  unctb  9065  infunabs  9067  infcda  9068  infdif  9069  infdif2  9070  infmap2  9078  ackbij2  9103  fictb  9105  cfslb  9126  fincssdom  9183  fin67  9255  fin1a2lem12  9271  axcclem  9317  dmct  9384  brdom3  9388  brdom5  9389  brdom4  9390  imadomg  9394  fnct  9397  mptct  9398  ondomon  9423  alephval2  9432  alephadd  9437  alephmul  9438  alephexp1  9439  alephsuc3  9440  alephexp2  9441  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  canthnum  9509  pwfseqlem5  9523  pwxpndom2  9525  pwcdandom  9527  gchaleph  9531  gchaleph2  9532  gchac  9541  winainflem  9553  gchina  9559  tsksdom  9616  tskinf  9629  inttsk  9634  inar1  9635  inatsk  9638  tskord  9640  tskcard  9641  grudomon  9677  gruina  9678  axgroth2  9685  axgroth6  9688  grothac  9690  hashun2  13210  hashss  13235  hashsslei  13251  isercoll  14442  o1fsum  14589  incexc2  14614  znnen  14985  qnnen  14986  rpnnen  15000  ruc  15016  phicl2  15520  phibnd  15523  4sqlem11  15706  vdwlem11  15742  0ram  15771  mreexdomd  16357  pgpssslw  18075  fislw  18086  cctop  20858  1stcfb  21296  2ndc1stc  21302  1stcrestlem  21303  2ndcctbss  21306  2ndcdisj2  21308  2ndcsep  21310  dis2ndc  21311  csdfil  21745  ufilen  21781  opnreen  22681  rectbntr0  22682  ovolctb2  23306  uniiccdif  23392  dyadmbl  23414  opnmblALT  23417  vitali  23427  mbfimaopnlem  23467  mbfsup  23476  fta1blem  23973  aannenlem3  24130  ppiwordi  24933  musum  24962  ppiub  24974  chpub  24990  dchrisum0re  25247  dirith2  25262  upgrex  26032  rabfodom  29470  abrexdomjm  29471  mptctf  29623  locfinreflem  30035  esumcst  30253  omsmeas  30513  sibfof  30530  subfaclefac  31284  erdszelem10  31308  snmlff  31437  finminlem  32437  phpreu  33523  lindsdom  33533  poimirlem26  33565  mblfinlem1  33576  abrexdom  33655  heiborlem3  33742  ctbnfien  37699  pellexlem4  37713  pellexlem5  37714  ttac  37920  idomodle  38091  idomsubgmo  38093  uzct  39546  smfaddlem2  41293  smfmullem4  41322  smfpimbor1lem1  41326  aacllem  42875
  Copyright terms: Public domain W3C validator