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

Theorem ssdomg 8542
 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 5203 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
2 simpr 488 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐵𝑉)
3 f1oi 6634 . . . . . . . . 9 ( I ↾ 𝐴):𝐴1-1-onto𝐴
4 dff1o3 6603 . . . . . . . . 9 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴)))
53, 4mpbi 233 . . . . . . . 8 (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴))
65simpli 487 . . . . . . 7 ( I ↾ 𝐴):𝐴onto𝐴
7 fof 6572 . . . . . . 7 (( I ↾ 𝐴):𝐴onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
86, 7ax-mp 5 . . . . . 6 ( I ↾ 𝐴):𝐴𝐴
9 fss 6508 . . . . . 6 ((( I ↾ 𝐴):𝐴𝐴𝐴𝐵) → ( I ↾ 𝐴):𝐴𝐵)
108, 9mpan 689 . . . . 5 (𝐴𝐵 → ( I ↾ 𝐴):𝐴𝐵)
11 funi 6366 . . . . . . 7 Fun I
12 cnvi 5978 . . . . . . . 8 I = I
1312funeqi 6355 . . . . . . 7 (Fun I ↔ Fun I )
1411, 13mpbir 234 . . . . . 6 Fun I
15 funres11 6410 . . . . . 6 (Fun I → Fun ( I ↾ 𝐴))
1614, 15ax-mp 5 . . . . 5 Fun ( I ↾ 𝐴)
17 df-f1 6339 . . . . 5 (( I ↾ 𝐴):𝐴1-1𝐵 ↔ (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
1810, 16, 17sylanblrc 593 . . . 4 (𝐴𝐵 → ( I ↾ 𝐴):𝐴1-1𝐵)
1918adantr 484 . . 3 ((𝐴𝐵𝐵𝑉) → ( I ↾ 𝐴):𝐴1-1𝐵)
20 f1dom2g 8514 . . 3 ((𝐴 ∈ V ∧ 𝐵𝑉 ∧ ( I ↾ 𝐴):𝐴1-1𝐵) → 𝐴𝐵)
211, 2, 19, 20syl3anc 1368 . 2 ((𝐴𝐵𝐵𝑉) → 𝐴𝐵)
2221expcom 417 1 (𝐵𝑉 → (𝐴𝐵𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  Vcvv 3469   ⊆ wss 3908   class class class wbr 5042   I cid 5436  ◡ccnv 5531   ↾ cres 5534  Fun wfun 6328  ⟶wf 6330  –1-1→wf1 6331  –onto→wfo 6332  –1-1-onto→wf1o 6333   ≼ cdom 8494 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-dom 8498 This theorem is referenced by:  cnvct  8573  ssct  8585  undom  8592  xpdom3  8602  domunsncan  8604  sucdom2  8614  0domg  8632  domtriord  8651  sdomel  8652  sdomdif  8653  onsdominel  8654  pwdom  8657  2pwuninel  8660  mapdom1  8670  mapdom3  8677  limenpsi  8680  php  8689  php2  8690  php3  8691  nndomog  8696  onomeneq  8697  unbnn  8762  nnsdomg  8765  fodomfi  8785  fidomdm  8789  pwfilem  8806  hartogslem1  8994  hartogs  8996  card2on  9006  wdompwdom  9030  wdom2d  9032  wdomima2g  9038  unxpwdom2  9040  unxpwdom  9041  harwdom  9043  r1sdom  9191  tskwe  9367  carddomi2  9387  cardsdomelir  9390  cardsdomel  9391  harcard  9395  carduni  9398  cardmin2  9416  infxpenlem  9428  ssnum  9454  acnnum  9467  fodomfi2  9475  inffien  9478  alephordi  9489  dfac12lem2  9559  djudoml  9599  cdainflem  9602  djuinf  9603  unctb  9616  infunabs  9618  infdju  9619  infdif  9620  infdif2  9621  infmap2  9629  ackbij2  9654  fictb  9656  cfslb  9677  fincssdom  9734  fin67  9806  fin1a2lem12  9822  axcclem  9868  dmct  9935  brdom3  9939  brdom5  9940  brdom4  9941  imadomg  9945  fnct  9948  mptct  9949  ondomon  9974  alephval2  9983  alephadd  9988  alephmul  9989  alephexp1  9990  alephsuc3  9991  alephexp2  9992  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  canthnum  10060  pwfseqlem5  10074  pwxpndom2  10076  pwdjundom  10078  gchaleph  10082  gchaleph2  10083  gchac  10092  winainflem  10104  gchina  10110  tsksdom  10167  tskinf  10180  inttsk  10185  inar1  10186  inatsk  10189  tskord  10191  tskcard  10192  grudomon  10228  gruina  10229  axgroth2  10236  axgroth6  10239  grothac  10241  hashun2  13740  hashss  13766  hashsslei  13783  isercoll  15015  o1fsum  15159  incexc2  15184  znnen  15556  qnnen  15557  rpnnen  15571  ruc  15587  phicl2  16094  phibnd  16097  4sqlem11  16280  vdwlem11  16316  0ram  16345  mreexdomd  16911  pgpssslw  18730  fislw  18741  cctop  21609  1stcfb  22048  2ndc1stc  22054  1stcrestlem  22055  2ndcctbss  22058  2ndcdisj2  22060  2ndcsep  22062  dis2ndc  22063  csdfil  22497  ufilen  22533  opnreen  23434  rectbntr0  23435  ovolctb2  24094  uniiccdif  24180  dyadmbl  24202  opnmblALT  24205  vitali  24215  mbfimaopnlem  24257  mbfsup  24266  fta1blem  24767  aannenlem3  24924  ppiwordi  25745  musum  25774  ppiub  25786  chpub  25802  dirith2  26110  upgrex  26883  rabfodom  30272  abrexdomjm  30273  mptctf  30463  locfinreflem  31162  esumcst  31396  omsmeas  31655  sibfof  31672  subfaclefac  32497  erdszelem10  32521  snmlff  32650  finminlem  33740  iccioo01  34702  isinf2  34783  pibt2  34795  phpreu  35003  lindsdom  35013  poimirlem26  35045  mblfinlem1  35056  abrexdom  35130  heiborlem3  35213  ctbnfien  39693  pellexlem4  39707  pellexlem5  39708  ttac  39911  idomodle  40074  idomsubgmo  40076  iscard5  40176  uzct  41635  smfaddlem2  43340  smfmullem4  43369  smfpimbor1lem1  43373  aacllem  45272
 Copyright terms: Public domain W3C validator