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

Theorem ssdomg 7144
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 4341 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 448 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5704 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5671 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 200 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 445 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5644 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 8 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5590 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 652 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5474 . . . . . . . 8  |-  Fun  _I
12 cnvi 5267 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5465 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 201 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5512 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 8 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 525 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5450 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 204 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 452 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7116 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1184 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 425 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   _Vcvv 2948    C_ wss 3312   class class class wbr 4204    _I cid 4485   `'ccnv 4868    |` cres 4871   Fun wfun 5439   -->wf 5441   -1-1->wf1 5442   -onto->wfo 5443   -1-1-onto->wf1o 5444    ~<_ cdom 7098
This theorem is referenced by:  undom  7187  xpdom3  7197  domunsncan  7199  0domg  7225  domtriord  7244  sdomel  7245  sdomdif  7246  onsdominel  7247  pwdom  7250  2pwuninel  7253  mapdom1  7263  mapdom3  7270  limenpsi  7273  php  7282  php2  7283  php3  7284  onomeneq  7287  nndomo  7291  sucdom2  7294  unbnn  7354  nnsdomg  7357  fodomfi  7376  fidomdm  7379  pwfilem  7392  hartogslem1  7500  hartogs  7502  card2on  7511  wdompwdom  7535  wdom2d  7537  wdomima2g  7543  unxpwdom2  7545  unxpwdom  7546  harwdom  7547  r1sdom  7689  tskwe  7826  carddomi2  7846  cardsdomelir  7849  cardsdomel  7850  harcard  7854  carduni  7857  cardmin2  7874  infxpenlem  7884  ssnum  7909  acnnum  7922  fodomfi2  7930  inffien  7933  alephordi  7944  dfac12lem2  8013  cdadom3  8057  cdainflem  8060  cdainf  8061  unctb  8074  infunabs  8076  infcda  8077  infdif  8078  infdif2  8079  infmap2  8087  ackbij2  8112  fictb  8114  cfslb  8135  fincssdom  8192  fin67  8264  fin1a2lem12  8280  axcclem  8326  brdom3  8395  brdom5  8396  brdom4  8397  imadomg  8401  ondomon  8427  alephval2  8436  alephadd  8441  alephmul  8442  alephexp1  8443  alephsuc3  8444  alephexp2  8445  alephreg  8446  pwcfsdom  8447  cfpwsdom  8448  canthnum  8513  pwfseqlem5  8527  pwxpndom2  8529  pwcdandom  8531  gchac  8537  gchaleph  8539  gchaleph2  8540  winainflem  8557  gchina  8563  tsksdom  8620  tskinf  8633  inttsk  8638  inar1  8639  inatsk  8642  tskord  8644  tskcard  8645  grudomon  8681  gruina  8682  axgroth2  8689  axgroth6  8692  grothac  8694  hashun2  11645  hashsslei  11673  isercoll  12449  o1fsum  12580  incexc2  12606  xpnnenOLD  12797  znnen  12800  qnnen  12801  rpnnen  12814  ruc  12830  phicl2  13145  phibnd  13148  4sqlem11  13311  vdwlem11  13347  0ram  13376  mreexdomd  13862  pgpssslw  15236  fislw  15247  cctop  17058  1stcfb  17496  2ndc1stc  17502  1stcrestlem  17503  2ndcctbss  17506  2ndcdisj2  17508  2ndcsep  17510  dis2ndc  17511  csdfil  17914  ufilen  17950  opnreen  18850  rectbntr0  18851  ovolctb2  19376  uniiccdif  19458  dyadmbl  19480  opnmblALT  19483  vitali  19493  mbfimaopnlem  19535  mbfsup  19544  fta1blem  20079  aannenlem3  20235  ppiwordi  20933  musum  20964  ppiub  20976  chpub  20992  dchrisum0re  21195  dirith2  21210  umgraex  21346  konigsberg  21697  abrexdomjm  23976  ssct  24089  fnct  24093  dmct  24094  cnvct  24095  mptct  24097  mptctf  24100  esumcst  24443  sibfof  24642  subfaclefac  24850  erdszelem10  24874  snmlff  25004  mblfinlem  26190  finminlem  26258  abrexdom  26369  heiborlem3  26459  ctbnfien  26816  pellexlem4  26832  pellexlem5  26833  ttac  27044  idomodle  27427  idomsubgmo  27429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-dom 7102
  Copyright terms: Public domain W3C validator