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

Theorem ssdomg 6902
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 4161 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 449 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5476 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5443 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 201 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 446 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5416 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 10 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5362 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 653 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5250 . . . . . . . 8  |-  Fun  _I
12 cnvi 5084 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5241 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 202 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5285 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 10 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 526 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5226 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 205 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 453 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 6874 . . 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 426 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   _Vcvv 2789    C_ wss 3153   class class class wbr 4024    _I cid 4303   `'ccnv 4687    |` cres 4690   Fun wfun 5215   -->wf 5217   -1-1->wf1 5218   -onto->wfo 5219   -1-1-onto->wf1o 5220    ~<_ cdom 6856
This theorem is referenced by:  undom  6945  xpdom3  6955  domunsncan  6957  0domg  6983  domtriord  7002  sdomel  7003  sdomdif  7004  onsdominel  7005  pwdom  7008  2pwuninel  7011  mapdom1  7021  mapdom3  7028  limenpsi  7031  php  7040  php2  7041  php3  7042  onomeneq  7045  nndomo  7049  sucdom2  7052  unbnn  7108  nnsdomg  7111  fodomfi  7130  fidomdm  7133  pwfilem  7145  hartogslem1  7252  hartogs  7254  card2on  7263  wdompwdom  7287  wdom2d  7289  wdomima2g  7295  unxpwdom2  7297  unxpwdom  7298  harwdom  7299  r1sdom  7441  tskwe  7578  carddomi2  7598  cardsdomelir  7601  cardsdomel  7602  harcard  7606  carduni  7609  cardmin2  7626  infxpenlem  7636  ssnum  7661  acnnum  7674  fodomfi2  7682  inffien  7685  alephordi  7696  dfac12lem2  7765  cdadom3  7809  cdainflem  7812  cdainf  7813  unctb  7826  infunabs  7828  infcda  7829  infdif  7830  infdif2  7831  infmap2  7839  ackbij2  7864  fictb  7866  cfslb  7887  fincssdom  7944  fin67  8016  fin1a2lem12  8032  axcclem  8078  brdom3  8148  brdom5  8149  brdom4  8150  imadomg  8154  ondomon  8180  alephval2  8189  alephadd  8194  alephmul  8195  alephexp1  8196  alephsuc3  8197  alephexp2  8198  alephreg  8199  pwcfsdom  8200  cfpwsdom  8201  canthnum  8266  pwfseqlem5  8280  pwxpndom2  8282  pwcdandom  8284  gchac  8290  gchaleph  8292  gchaleph2  8293  winainflem  8310  gchina  8316  tsksdom  8373  tskinf  8386  inttsk  8391  inar1  8392  inatsk  8395  tskord  8397  tskcard  8398  grudomon  8434  gruina  8435  axgroth2  8442  axgroth6  8445  grothac  8447  hashun2  11359  hashsslei  11372  isercoll  12135  o1fsum  12265  incexc2  12291  xpnnenOLD  12482  znnen  12485  qnnen  12486  rpnnen  12499  ruc  12515  phicl2  12830  phibnd  12833  4sqlem11  12996  vdwlem11  13032  0ram  13061  mreexdomd  13545  pgpssslw  14919  fislw  14930  cctop  16737  1stcfb  17165  2ndc1stc  17171  1stcrestlem  17172  2ndcctbss  17175  2ndcdisj2  17177  2ndcsep  17179  dis2ndc  17180  csdfil  17583  ufilen  17619  opnreen  18330  rectbntr0  18331  ovolctb2  18845  uniiccdif  18927  dyadmbl  18949  opnmblALT  18952  vitali  18962  mbfimaopnlem  19004  mbfsup  19013  fta1blem  19548  aannenlem3  19704  ppiwordi  20394  musum  20425  ppiub  20437  chpub  20453  dchrisum0re  20656  dirith2  20671  subfaclefac  23111  erdszelem10  23135  umgraex  23279  konigsberg  23315  snmlff  23316  sndw  24498  carinttar  25301  finminlem  25630  abrexdom  25804  heiborlem3  25936  ctbnfien  26300  pellexlem4  26316  pellexlem5  26317  ttac  26528  idomodle  26911  idomsubgmo  26913
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-dom 6860
  Copyright terms: Public domain W3C validator