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

Theorem ssdomg 7561
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 4593 . . 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 5851 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5822 . . . . . . . . . 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 5795 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5739 . . . . . . 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 5618 . . . . . . . 8  |-  Fun  _I
12 cnvi 5410 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5608 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 209 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5656 . . . . . . 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 5593 . . . . 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 7533 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1228 . 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 1767   _Vcvv 3113    C_ wss 3476   class class class wbr 4447    _I cid 4790   `'ccnv 4998    |` cres 5001   Fun wfun 5582   -->wf 5584   -1-1->wf1 5585   -onto->wfo 5586   -1-1-onto->wf1o 5587    ~<_ cdom 7514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-dom 7518
This theorem is referenced by:  undom  7605  xpdom3  7615  domunsncan  7617  0domg  7644  domtriord  7663  sdomel  7664  sdomdif  7665  onsdominel  7666  pwdom  7669  2pwuninel  7672  mapdom1  7682  mapdom3  7689  limenpsi  7692  php  7701  php2  7702  php3  7703  onomeneq  7707  nndomo  7711  sucdom2  7714  unbnn  7776  nnsdomg  7779  fodomfi  7799  fidomdm  7802  pwfilem  7814  hartogslem1  7967  hartogs  7969  card2on  7980  wdompwdom  8004  wdom2d  8006  wdomima2g  8012  unxpwdom2  8014  unxpwdom  8015  harwdom  8016  r1sdom  8192  tskwe  8331  carddomi2  8351  cardsdomelir  8354  cardsdomel  8355  harcard  8359  carduni  8362  cardmin2  8379  infxpenlem  8391  ssnum  8420  acnnum  8433  fodomfi2  8441  inffien  8444  alephordi  8455  dfac12lem2  8524  cdadom3  8568  cdainflem  8571  cdainf  8572  unctb  8585  infunabs  8587  infcda  8588  infdif  8589  infdif2  8590  infmap2  8598  ackbij2  8623  fictb  8625  cfslb  8646  fincssdom  8703  fin67  8775  fin1a2lem12  8791  axcclem  8837  brdom3  8906  brdom5  8907  brdom4  8908  imadomg  8912  ondomon  8938  alephval2  8947  alephadd  8952  alephmul  8953  alephexp1  8954  alephsuc3  8955  alephexp2  8956  alephreg  8957  pwcfsdom  8958  cfpwsdom  8959  canthnum  9027  pwfseqlem5  9041  pwxpndom2  9043  pwcdandom  9045  gchaleph  9049  gchaleph2  9050  gchac  9059  winainflem  9071  gchina  9077  tsksdom  9134  tskinf  9147  inttsk  9152  inar1  9153  inatsk  9156  tskord  9158  tskcard  9159  grudomon  9195  gruina  9196  axgroth2  9203  axgroth6  9206  grothac  9208  hashun2  12419  hashss  12439  hashsslei  12449  isercoll  13453  o1fsum  13590  incexc2  13613  xpnnenOLD  13804  znnen  13807  qnnen  13808  rpnnen  13821  ruc  13837  phicl2  14157  phibnd  14160  4sqlem11  14332  vdwlem11  14368  0ram  14397  mreexdomd  14904  pgpssslw  16440  fislw  16451  cctop  19301  1stcfb  19740  2ndc1stc  19746  1stcrestlem  19747  2ndcctbss  19750  2ndcdisj2  19752  2ndcsep  19754  dis2ndc  19755  csdfil  20158  ufilen  20194  opnreen  21099  rectbntr0  21100  ovolctb2  21666  uniiccdif  21750  dyadmbl  21772  opnmblALT  21775  vitali  21785  mbfimaopnlem  21825  mbfsup  21834  fta1blem  22332  aannenlem3  22488  ppiwordi  23192  musum  23223  ppiub  23235  chpub  23251  dchrisum0re  23454  dirith2  23469  umgraex  24027  konigsberg  24691  abrexdomjm  27107  ssct  27232  fnct  27236  dmct  27237  cnvct  27238  mptct  27241  mptctf  27244  esumcst  27739  sibfof  27950  subfaclefac  28288  erdszelem10  28312  snmlff  28442  mblfinlem1  29656  finminlem  29741  abrexdom  29852  heiborlem3  29940  ctbnfien  30384  pellexlem4  30400  pellexlem5  30401  ttac  30610  idomodle  30786  idomsubgmo  30788
  Copyright terms: Public domain W3C validator