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

Theorem ssdomg 7620
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 4568 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 463 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5864 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5835 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 212 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 460 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5808 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5752 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 675 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5629 . . . . . . . 8  |-  Fun  _I
12 cnvi 5257 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5619 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 213 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5667 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 5 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 541 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5604 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 216 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 467 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7592 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1265 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 437 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1869   _Vcvv 3082    C_ wss 3437   class class class wbr 4421    _I cid 4761   `'ccnv 4850    |` cres 4853   Fun wfun 5593   -->wf 5595   -1-1->wf1 5596   -onto->wfo 5597   -1-1-onto->wf1o 5598    ~<_ cdom 7573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-dom 7577
This theorem is referenced by:  undom  7664  xpdom3  7674  domunsncan  7676  0domg  7703  domtriord  7722  sdomel  7723  sdomdif  7724  onsdominel  7725  pwdom  7728  2pwuninel  7731  mapdom1  7741  mapdom3  7748  limenpsi  7751  php  7760  php2  7761  php3  7762  onomeneq  7766  nndomo  7770  sucdom2  7772  unbnn  7831  nnsdomg  7834  fodomfi  7854  fidomdm  7857  pwfilem  7872  hartogslem1  8061  hartogs  8063  card2on  8073  wdompwdom  8097  wdom2d  8099  wdomima2g  8105  unxpwdom2  8107  unxpwdom  8108  harwdom  8109  r1sdom  8248  tskwe  8387  carddomi2  8407  cardsdomelir  8410  cardsdomel  8411  harcard  8415  carduni  8418  cardmin2  8435  infxpenlem  8447  ssnum  8472  acnnum  8485  fodomfi2  8493  inffien  8496  alephordi  8507  dfac12lem2  8576  cdadom3  8620  cdainflem  8623  cdainf  8624  unctb  8637  infunabs  8639  infcda  8640  infdif  8641  infdif2  8642  infmap2  8650  ackbij2  8675  fictb  8677  cfslb  8698  fincssdom  8755  fin67  8827  fin1a2lem12  8843  axcclem  8889  brdom3  8958  brdom5  8959  brdom4  8960  imadomg  8964  ondomon  8990  alephval2  8999  alephadd  9004  alephmul  9005  alephexp1  9006  alephsuc3  9007  alephexp2  9008  alephreg  9009  pwcfsdom  9010  cfpwsdom  9011  canthnum  9076  pwfseqlem5  9090  pwxpndom2  9092  pwcdandom  9094  gchaleph  9098  gchaleph2  9099  gchac  9108  winainflem  9120  gchina  9126  tsksdom  9183  tskinf  9196  inttsk  9201  inar1  9202  inatsk  9205  tskord  9207  tskcard  9208  grudomon  9244  gruina  9245  axgroth2  9252  axgroth6  9255  grothac  9257  hashun2  12563  hashss  12587  hashsslei  12597  isercoll  13724  o1fsum  13866  incexc2  13889  znnen  14258  qnnen  14259  rpnnen  14272  ruc  14288  phicl2  14709  phibnd  14712  4sqlem11  14892  vdwlem11  14934  0ram  14971  mreexdomd  15548  pgpssslw  17259  fislw  17270  cctop  20013  1stcfb  20452  2ndc1stc  20458  1stcrestlem  20459  2ndcctbss  20462  2ndcdisj2  20464  2ndcsep  20466  dis2ndc  20467  csdfil  20901  ufilen  20937  opnreen  21841  rectbntr0  21842  ovolctb2  22437  uniiccdif  22527  dyadmbl  22550  opnmblALT  22553  vitali  22563  mbfimaopnlem  22603  mbfsup  22612  fta1blem  23111  aannenlem3  23278  ppiwordi  24081  musum  24112  ppiub  24124  chpub  24140  dchrisum0re  24343  dirith2  24358  umgraex  25042  konigsberg  25707  rabfodom  28133  abrexdomjm  28134  ssct  28293  fnct  28297  dmct  28298  cnvct  28299  mptct  28302  mptctf  28305  locfinreflem  28669  esumcst  28886  omsmeas  29157  omsmeasOLD  29158  sibfof  29175  subfaclefac  29901  erdszelem10  29925  snmlff  30054  finminlem  30973  phpreu  31887  poimirlem26  31924  mblfinlem1  31935  abrexdom  32015  heiborlem3  32103  ctbnfien  35624  pellexlem4  35640  pellexlem5  35641  ttac  35855  idomodle  36034  idomsubgmo  36036  uzct  37311  umgrex  38889  aacllem  39884
  Copyright terms: Public domain W3C validator