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

Theorem ssdomg 7376
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 4459 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 461 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5697 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5668 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 208 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 458 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5641 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5588 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 670 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5469 . . . . . . . 8  |-  Fun  _I
12 cnvi 5262 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5459 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 209 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5507 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 5 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 538 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5444 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 212 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 465 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7348 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1218 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 435 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   _Vcvv 2993    C_ wss 3349   class class class wbr 4313    _I cid 4652   `'ccnv 4860    |` cres 4863   Fun wfun 5433   -->wf 5435   -1-1->wf1 5436   -onto->wfo 5437   -1-1-onto->wf1o 5438    ~<_ cdom 7329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-dom 7333
This theorem is referenced by:  undom  7420  xpdom3  7430  domunsncan  7432  0domg  7459  domtriord  7478  sdomel  7479  sdomdif  7480  onsdominel  7481  pwdom  7484  2pwuninel  7487  mapdom1  7497  mapdom3  7504  limenpsi  7507  php  7516  php2  7517  php3  7518  onomeneq  7521  nndomo  7525  sucdom2  7528  unbnn  7589  nnsdomg  7592  fodomfi  7611  fidomdm  7614  pwfilem  7626  hartogslem1  7777  hartogs  7779  card2on  7790  wdompwdom  7814  wdom2d  7816  wdomima2g  7822  unxpwdom2  7824  unxpwdom  7825  harwdom  7826  r1sdom  8002  tskwe  8141  carddomi2  8161  cardsdomelir  8164  cardsdomel  8165  harcard  8169  carduni  8172  cardmin2  8189  infxpenlem  8201  ssnum  8230  acnnum  8243  fodomfi2  8251  inffien  8254  alephordi  8265  dfac12lem2  8334  cdadom3  8378  cdainflem  8381  cdainf  8382  unctb  8395  infunabs  8397  infcda  8398  infdif  8399  infdif2  8400  infmap2  8408  ackbij2  8433  fictb  8435  cfslb  8456  fincssdom  8513  fin67  8585  fin1a2lem12  8601  axcclem  8647  brdom3  8716  brdom5  8717  brdom4  8718  imadomg  8722  ondomon  8748  alephval2  8757  alephadd  8762  alephmul  8763  alephexp1  8764  alephsuc3  8765  alephexp2  8766  alephreg  8767  pwcfsdom  8768  cfpwsdom  8769  canthnum  8837  pwfseqlem5  8851  pwxpndom2  8853  pwcdandom  8855  gchaleph  8859  gchaleph2  8860  gchac  8869  winainflem  8881  gchina  8887  tsksdom  8944  tskinf  8957  inttsk  8962  inar1  8963  inatsk  8966  tskord  8968  tskcard  8969  grudomon  9005  gruina  9006  axgroth2  9013  axgroth6  9016  grothac  9018  hashun2  12167  hashss  12187  hashsslei  12197  isercoll  13166  o1fsum  13297  incexc2  13322  xpnnenOLD  13513  znnen  13516  qnnen  13517  rpnnen  13530  ruc  13546  phicl2  13864  phibnd  13867  4sqlem11  14037  vdwlem11  14073  0ram  14102  mreexdomd  14608  pgpssslw  16134  fislw  16145  cctop  18632  1stcfb  19071  2ndc1stc  19077  1stcrestlem  19078  2ndcctbss  19081  2ndcdisj2  19083  2ndcsep  19085  dis2ndc  19086  csdfil  19489  ufilen  19525  opnreen  20430  rectbntr0  20431  ovolctb2  20997  uniiccdif  21080  dyadmbl  21102  opnmblALT  21105  vitali  21115  mbfimaopnlem  21155  mbfsup  21164  fta1blem  21662  aannenlem3  21818  ppiwordi  22522  musum  22553  ppiub  22565  chpub  22581  dchrisum0re  22784  dirith2  22799  umgraex  23279  konigsberg  23630  abrexdomjm  25910  ssct  26031  fnct  26035  dmct  26036  cnvct  26037  mptct  26040  mptctf  26043  esumcst  26536  sibfof  26748  subfaclefac  27086  erdszelem10  27110  snmlff  27240  mblfinlem1  28454  finminlem  28539  abrexdom  28650  heiborlem3  28738  ctbnfien  29183  pellexlem4  29199  pellexlem5  29200  ttac  29411  idomodle  29587  idomsubgmo  29589
  Copyright terms: Public domain W3C validator