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

Theorem ssdomg 7559
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 4579 . . 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 5837 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5808 . . . . . . . . . 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 5781 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5725 . . . . . . 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 5604 . . . . . . . 8  |-  Fun  _I
12 cnvi 5396 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5594 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 209 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5642 . . . . . . 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 5579 . . . . 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 7531 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1227 . 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 1802   _Vcvv 3093    C_ wss 3458   class class class wbr 4433    _I cid 4776   `'ccnv 4984    |` cres 4987   Fun wfun 5568   -->wf 5570   -1-1->wf1 5571   -onto->wfo 5572   -1-1-onto->wf1o 5573    ~<_ cdom 7512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-dom 7516
This theorem is referenced by:  undom  7603  xpdom3  7613  domunsncan  7615  0domg  7642  domtriord  7661  sdomel  7662  sdomdif  7663  onsdominel  7664  pwdom  7667  2pwuninel  7670  mapdom1  7680  mapdom3  7687  limenpsi  7690  php  7699  php2  7700  php3  7701  onomeneq  7705  nndomo  7709  sucdom2  7712  unbnn  7774  nnsdomg  7777  fodomfi  7797  fidomdm  7800  pwfilem  7812  hartogslem1  7965  hartogs  7967  card2on  7978  wdompwdom  8002  wdom2d  8004  wdomima2g  8010  unxpwdom2  8012  unxpwdom  8013  harwdom  8014  r1sdom  8190  tskwe  8329  carddomi2  8349  cardsdomelir  8352  cardsdomel  8353  harcard  8357  carduni  8360  cardmin2  8377  infxpenlem  8389  ssnum  8418  acnnum  8431  fodomfi2  8439  inffien  8442  alephordi  8453  dfac12lem2  8522  cdadom3  8566  cdainflem  8569  cdainf  8570  unctb  8583  infunabs  8585  infcda  8586  infdif  8587  infdif2  8588  infmap2  8596  ackbij2  8621  fictb  8623  cfslb  8644  fincssdom  8701  fin67  8773  fin1a2lem12  8789  axcclem  8835  brdom3  8904  brdom5  8905  brdom4  8906  imadomg  8910  ondomon  8936  alephval2  8945  alephadd  8950  alephmul  8951  alephexp1  8952  alephsuc3  8953  alephexp2  8954  alephreg  8955  pwcfsdom  8956  cfpwsdom  8957  canthnum  9025  pwfseqlem5  9039  pwxpndom2  9041  pwcdandom  9043  gchaleph  9047  gchaleph2  9048  gchac  9057  winainflem  9069  gchina  9075  tsksdom  9132  tskinf  9145  inttsk  9150  inar1  9151  inatsk  9154  tskord  9156  tskcard  9157  grudomon  9193  gruina  9194  axgroth2  9201  axgroth6  9204  grothac  9206  hashun2  12425  hashss  12448  hashsslei  12458  isercoll  13464  o1fsum  13601  incexc2  13624  xpnnenOLD  13815  znnen  13818  qnnen  13819  rpnnen  13832  ruc  13848  phicl2  14170  phibnd  14173  4sqlem11  14345  vdwlem11  14381  0ram  14410  mreexdomd  14918  pgpssslw  16503  fislw  16514  cctop  19373  1stcfb  19812  2ndc1stc  19818  1stcrestlem  19819  2ndcctbss  19822  2ndcdisj2  19824  2ndcsep  19826  dis2ndc  19827  csdfil  20261  ufilen  20297  opnreen  21202  rectbntr0  21203  ovolctb2  21769  uniiccdif  21853  dyadmbl  21875  opnmblALT  21878  vitali  21888  mbfimaopnlem  21928  mbfsup  21937  fta1blem  22435  aannenlem3  22591  ppiwordi  23301  musum  23332  ppiub  23344  chpub  23360  dchrisum0re  23563  dirith2  23578  umgraex  24188  konigsberg  24852  rabfodom  27269  abrexdomjm  27270  ssct  27397  fnct  27401  dmct  27402  cnvct  27403  mptct  27406  mptctf  27409  locfinreflem  27709  esumcst  27937  sibfof  28148  subfaclefac  28486  erdszelem10  28510  snmlff  28640  mblfinlem1  30019  finminlem  30104  abrexdom  30189  heiborlem3  30277  ctbnfien  30720  pellexlem4  30736  pellexlem5  30737  ttac  30946  idomodle  31122  idomsubgmo  31124
  Copyright terms: Public domain W3C validator