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

Theorem ssdomg 8947
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 5285 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
2 simpr 486 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐵𝑉)
3 f1oi 6827 . . . . . . . . 9 ( I ↾ 𝐴):𝐴1-1-onto𝐴
4 dff1o3 6795 . . . . . . . . 9 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴)))
53, 4mpbi 229 . . . . . . . 8 (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴))
65simpli 485 . . . . . . 7 ( I ↾ 𝐴):𝐴onto𝐴
7 fof 6761 . . . . . . 7 (( I ↾ 𝐴):𝐴onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
86, 7ax-mp 5 . . . . . 6 ( I ↾ 𝐴):𝐴𝐴
9 fss 6690 . . . . . 6 ((( I ↾ 𝐴):𝐴𝐴𝐴𝐵) → ( I ↾ 𝐴):𝐴𝐵)
108, 9mpan 689 . . . . 5 (𝐴𝐵 → ( I ↾ 𝐴):𝐴𝐵)
11 funi 6538 . . . . . . 7 Fun I
12 cnvi 6099 . . . . . . . 8 I = I
1312funeqi 6527 . . . . . . 7 (Fun I ↔ Fun I )
1411, 13mpbir 230 . . . . . 6 Fun I
15 funres11 6583 . . . . . 6 (Fun I → Fun ( I ↾ 𝐴))
1614, 15ax-mp 5 . . . . 5 Fun ( I ↾ 𝐴)
17 df-f1 6506 . . . . 5 (( I ↾ 𝐴):𝐴1-1𝐵 ↔ (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
1810, 16, 17sylanblrc 591 . . . 4 (𝐴𝐵 → ( I ↾ 𝐴):𝐴1-1𝐵)
1918adantr 482 . . 3 ((𝐴𝐵𝐵𝑉) → ( I ↾ 𝐴):𝐴1-1𝐵)
20 f1dom2g 8916 . . 3 ((𝐴 ∈ V ∧ 𝐵𝑉 ∧ ( I ↾ 𝐴):𝐴1-1𝐵) → 𝐴𝐵)
211, 2, 19, 20syl3anc 1372 . 2 ((𝐴𝐵𝐵𝑉) → 𝐴𝐵)
2221expcom 415 1 (𝐵𝑉 → (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Vcvv 3448  wss 3915   class class class wbr 5110   I cid 5535  ccnv 5637  cres 5640  Fun wfun 6495  wf 6497  1-1wf1 6498  ontowfo 6499  1-1-ontowf1o 6500  cdom 8888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-dom 8892
This theorem is referenced by:  cnvct  8985  ssctOLD  9003  undomOLD  9011  xpdom3  9021  domunsncan  9023  sucdom2OLD  9033  0domgOLD  9052  domtriord  9074  sdomel  9075  sdomdif  9076  onsdominel  9077  pwdom  9080  2pwuninel  9083  mapdom1  9093  mapdom3  9100  limenpsi  9103  phpOLD  9173  php2OLD  9174  php3OLD  9175  nndomogOLD  9177  onomeneqOLD  9180  unbnn  9250  nnsdomgOLD  9254  fodomfi  9276  fidomdm  9280  pwfilemOLD  9297  hartogslem1  9485  hartogs  9487  card2on  9497  wdompwdom  9521  wdom2d  9523  wdomima2g  9529  unxpwdom2  9531  unxpwdom  9532  harwdom  9534  r1sdom  9717  tskwe  9893  carddomi2  9913  cardsdomelir  9916  cardsdomel  9917  harcard  9921  carduni  9924  cardmin2  9942  infxpenlem  9956  ssnum  9982  acnnum  9995  fodomfi2  10003  inffien  10006  alephordi  10017  dfac12lem2  10087  djudoml  10127  cdainflem  10130  djuinf  10131  unctb  10148  infunabs  10150  infdju  10151  infdif  10152  infdif2  10153  infmap2  10161  ackbij2  10186  fictb  10188  cfslb  10209  fincssdom  10266  fin67  10338  fin1a2lem12  10354  axcclem  10400  dmct  10467  brdom3  10471  brdom5  10472  brdom4  10473  imadomg  10477  fnct  10480  mptct  10481  ondomon  10506  alephval2  10515  alephadd  10520  alephmul  10521  alephexp1  10522  alephsuc3  10523  alephexp2  10524  alephreg  10525  pwcfsdom  10526  cfpwsdom  10527  canthnum  10592  pwfseqlem5  10606  pwxpndom2  10608  pwdjundom  10610  gchaleph  10614  gchaleph2  10615  gchac  10624  winainflem  10636  gchina  10642  tsksdom  10699  tskinf  10712  inttsk  10717  inar1  10718  inatsk  10721  tskord  10723  tskcard  10724  grudomon  10760  gruina  10761  axgroth2  10768  axgroth6  10771  grothac  10773  hashun2  14290  hashss  14316  hashsslei  14333  isercoll  15559  o1fsum  15705  incexc2  15730  znnen  16101  qnnen  16102  rpnnen  16116  ruc  16132  phicl2  16647  phibnd  16650  4sqlem11  16834  vdwlem11  16870  0ram  16899  mreexdomd  17536  pgpssslw  19403  fislw  19414  cctop  22372  1stcfb  22812  2ndc1stc  22818  1stcrestlem  22819  2ndcctbss  22822  2ndcdisj2  22824  2ndcsep  22826  dis2ndc  22827  csdfil  23261  ufilen  23297  opnreen  24210  rectbntr0  24211  ovolctb2  24872  uniiccdif  24958  dyadmbl  24980  opnmblALT  24983  vitali  24993  mbfimaopnlem  25035  mbfsup  25044  fta1blem  25549  aannenlem3  25706  ppiwordi  26527  musum  26556  ppiub  26568  chpub  26584  dirith2  26892  upgrex  28085  rabfodom  31474  abrexdomjm  31475  mptctf  31676  locfinreflem  32461  esumcst  32702  omsmeas  32963  sibfof  32980  subfaclefac  33810  erdszelem10  33834  snmlff  33963  finminlem  34819  iccioo01  35827  isinf2  35905  pibt2  35917  phpreu  36091  lindsdom  36101  poimirlem26  36133  mblfinlem1  36144  abrexdom  36218  heiborlem3  36301  ctbnfien  41170  pellexlem4  41184  pellexlem5  41185  ttac  41389  idomodle  41552  idomsubgmo  41554  iscard5  41882  uzct  43345  rn1st  43576  smfaddlem2  45079  smfmullem4  45109  smfpimbor1lem1  45113  aacllem  47322
  Copyright terms: Public domain W3C validator