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

Theorem ssdomg 7554
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 4583 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 459 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5833 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5804 . . . . . . . . . 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 456 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5777 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 5 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5721 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 668 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5600 . . . . . . . 8  |-  Fun  _I
12 cnvi 5395 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5590 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 209 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5638 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 5 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 536 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5575 . . . . 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 463 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7526 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1226 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 433 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   _Vcvv 3106    C_ wss 3461   class class class wbr 4439    _I cid 4779   `'ccnv 4987    |` cres 4990   Fun wfun 5564   -->wf 5566   -1-1->wf1 5567   -onto->wfo 5568   -1-1-onto->wf1o 5569    ~<_ cdom 7507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-dom 7511
This theorem is referenced by:  undom  7598  xpdom3  7608  domunsncan  7610  0domg  7637  domtriord  7656  sdomel  7657  sdomdif  7658  onsdominel  7659  pwdom  7662  2pwuninel  7665  mapdom1  7675  mapdom3  7682  limenpsi  7685  php  7694  php2  7695  php3  7696  onomeneq  7700  nndomo  7704  sucdom2  7707  unbnn  7768  nnsdomg  7771  fodomfi  7791  fidomdm  7794  pwfilem  7806  hartogslem1  7959  hartogs  7961  card2on  7972  wdompwdom  7996  wdom2d  7998  wdomima2g  8004  unxpwdom2  8006  unxpwdom  8007  harwdom  8008  r1sdom  8183  tskwe  8322  carddomi2  8342  cardsdomelir  8345  cardsdomel  8346  harcard  8350  carduni  8353  cardmin2  8370  infxpenlem  8382  ssnum  8411  acnnum  8424  fodomfi2  8432  inffien  8435  alephordi  8446  dfac12lem2  8515  cdadom3  8559  cdainflem  8562  cdainf  8563  unctb  8576  infunabs  8578  infcda  8579  infdif  8580  infdif2  8581  infmap2  8589  ackbij2  8614  fictb  8616  cfslb  8637  fincssdom  8694  fin67  8766  fin1a2lem12  8782  axcclem  8828  brdom3  8897  brdom5  8898  brdom4  8899  imadomg  8903  ondomon  8929  alephval2  8938  alephadd  8943  alephmul  8944  alephexp1  8945  alephsuc3  8946  alephexp2  8947  alephreg  8948  pwcfsdom  8949  cfpwsdom  8950  canthnum  9016  pwfseqlem5  9030  pwxpndom2  9032  pwcdandom  9034  gchaleph  9038  gchaleph2  9039  gchac  9048  winainflem  9060  gchina  9066  tsksdom  9123  tskinf  9136  inttsk  9141  inar1  9142  inatsk  9145  tskord  9147  tskcard  9148  grudomon  9184  gruina  9185  axgroth2  9192  axgroth6  9195  grothac  9197  hashun2  12434  hashss  12458  hashsslei  12468  isercoll  13572  o1fsum  13709  incexc2  13732  xpnnenOLD  14027  znnen  14030  qnnen  14031  rpnnen  14044  ruc  14060  phicl2  14382  phibnd  14385  4sqlem11  14557  vdwlem11  14593  0ram  14622  mreexdomd  15138  pgpssslw  16833  fislw  16844  cctop  19674  1stcfb  20112  2ndc1stc  20118  1stcrestlem  20119  2ndcctbss  20122  2ndcdisj2  20124  2ndcsep  20126  dis2ndc  20127  csdfil  20561  ufilen  20597  opnreen  21502  rectbntr0  21503  ovolctb2  22069  uniiccdif  22153  dyadmbl  22175  opnmblALT  22178  vitali  22188  mbfimaopnlem  22228  mbfsup  22237  fta1blem  22735  aannenlem3  22892  ppiwordi  23634  musum  23665  ppiub  23677  chpub  23693  dchrisum0re  23896  dirith2  23911  umgraex  24525  konigsberg  25189  rabfodom  27603  abrexdomjm  27604  ssct  27762  fnct  27766  dmct  27767  cnvct  27768  mptct  27771  mptctf  27774  locfinreflem  28078  esumcst  28292  omsmeas  28531  sibfof  28546  subfaclefac  28884  erdszelem10  28908  snmlff  29038  mblfinlem1  30291  finminlem  30376  abrexdom  30461  heiborlem3  30549  ctbnfien  30991  pellexlem4  31007  pellexlem5  31008  ttac  31217  idomodle  31394  idomsubgmo  31396  aacllem  33604
  Copyright terms: Public domain W3C validator