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

Theorem ssdomg 7633
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  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )

Proof of Theorem ssdomg
StepHypRef Expression
1 ssexg 4542 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 468 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5864 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5834 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 213 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 465 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5806 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5749 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 684 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5619 . . . . . . . 8  |-  Fun  _I
12 cnvi 5246 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5609 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 214 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5661 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 5 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 547 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5594 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 217 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 472 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7605 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1292 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 442 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    e. wcel 1904   _Vcvv 3031    C_ wss 3390   class class class wbr 4395    _I cid 4749   `'ccnv 4838    |` cres 4841   Fun wfun 5583   -->wf 5585   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588    ~<_ cdom 7585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-dom 7589
This theorem is referenced by:  ssct  7671  undom  7678  xpdom3  7688  domunsncan  7690  0domg  7717  domtriord  7736  sdomel  7737  sdomdif  7738  onsdominel  7739  pwdom  7742  2pwuninel  7745  mapdom1  7755  mapdom3  7762  limenpsi  7765  php  7774  php2  7775  php3  7776  onomeneq  7780  nndomo  7784  sucdom2  7786  unbnn  7845  nnsdomg  7848  fodomfi  7868  fidomdm  7871  pwfilem  7886  hartogslem1  8075  hartogs  8077  card2on  8087  wdompwdom  8111  wdom2d  8113  wdomima2g  8119  unxpwdom2  8121  unxpwdom  8122  harwdom  8123  r1sdom  8263  tskwe  8402  carddomi2  8422  cardsdomelir  8425  cardsdomel  8426  harcard  8430  carduni  8433  cardmin2  8450  infxpenlem  8462  ssnum  8488  acnnum  8501  fodomfi2  8509  inffien  8512  alephordi  8523  dfac12lem2  8592  cdadom3  8636  cdainflem  8639  cdainf  8640  unctb  8653  infunabs  8655  infcda  8656  infdif  8657  infdif2  8658  infmap2  8666  ackbij2  8691  fictb  8693  cfslb  8714  fincssdom  8771  fin67  8843  fin1a2lem12  8859  axcclem  8905  brdom3  8974  brdom5  8975  brdom4  8976  imadomg  8980  ondomon  9006  alephval2  9015  alephadd  9020  alephmul  9021  alephexp1  9022  alephsuc3  9023  alephexp2  9024  alephreg  9025  pwcfsdom  9026  cfpwsdom  9027  canthnum  9092  pwfseqlem5  9106  pwxpndom2  9108  pwcdandom  9110  gchaleph  9114  gchaleph2  9115  gchac  9124  winainflem  9136  gchina  9142  tsksdom  9199  tskinf  9212  inttsk  9217  inar1  9218  inatsk  9221  tskord  9223  tskcard  9224  grudomon  9260  gruina  9261  axgroth2  9268  axgroth6  9271  grothac  9273  hashun2  12600  hashss  12624  hashsslei  12639  isercoll  13808  o1fsum  13950  incexc2  13973  znnen  14342  qnnen  14343  rpnnen  14356  ruc  14372  phicl2  14795  phibnd  14798  4sqlem11  14978  vdwlem11  15020  0ram  15057  mreexdomd  15633  pgpssslw  17344  fislw  17355  cctop  20098  1stcfb  20537  2ndc1stc  20543  1stcrestlem  20544  2ndcctbss  20547  2ndcdisj2  20549  2ndcsep  20551  dis2ndc  20552  csdfil  20987  ufilen  21023  opnreen  21927  rectbntr0  21928  ovolctb2  22523  uniiccdif  22614  dyadmbl  22637  opnmblALT  22640  vitali  22650  mbfimaopnlem  22690  mbfsup  22699  fta1blem  23198  aannenlem3  23365  ppiwordi  24168  musum  24199  ppiub  24211  chpub  24227  dchrisum0re  24430  dirith2  24445  umgraex  25129  konigsberg  25794  rabfodom  28219  abrexdomjm  28220  fnct  28372  dmct  28373  cnvct  28374  mptct  28377  mptctf  28380  locfinreflem  28741  esumcst  28958  omsmeas  29228  omsmeasOLD  29229  sibfof  29246  subfaclefac  29971  erdszelem10  29995  snmlff  30124  finminlem  31045  phpreu  31993  poimirlem26  32030  mblfinlem1  32041  abrexdom  32121  heiborlem3  32209  ctbnfien  35732  pellexlem4  35747  pellexlem5  35748  ttac  35962  idomodle  36141  idomsubgmo  36143  uzct  37463  upgrex  39338  aacllem  41046
  Copyright terms: Public domain W3C validator