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

Theorem divslem 14493
Description: The function in divsval 14492 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
Hypotheses
Ref Expression
divsval.u  |-  ( ph  ->  U  =  ( R 
/.s  .~  ) )
divsval.v  |-  ( ph  ->  V  =  ( Base `  R ) )
divsval.f  |-  F  =  ( x  e.  V  |->  [ x ]  .~  )
divsval.e  |-  ( ph  ->  .~  e.  W )
divsval.r  |-  ( ph  ->  R  e.  Z )
Assertion
Ref Expression
divslem  |-  ( ph  ->  F : V -onto-> ( V /.  .~  ) )
Distinct variable groups:    x,  .~    ph, x    x, R    x, V
Allowed substitution hints:    U( x)    F( x)    W( x)    Z( x)

Proof of Theorem divslem
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 divsval.e . . . . . 6  |-  ( ph  ->  .~  e.  W )
2 ecexg 7117 . . . . . 6  |-  (  .~  e.  W  ->  [ x ]  .~  e.  _V )
31, 2syl 16 . . . . 5  |-  ( ph  ->  [ x ]  .~  e.  _V )
43ralrimivw 2812 . . . 4  |-  ( ph  ->  A. x  e.  V  [ x ]  .~  e.  _V )
5 divsval.f . . . . 5  |-  F  =  ( x  e.  V  |->  [ x ]  .~  )
65fnmpt 5549 . . . 4  |-  ( A. x  e.  V  [
x ]  .~  e.  _V  ->  F  Fn  V
)
74, 6syl 16 . . 3  |-  ( ph  ->  F  Fn  V )
8 dffn4 5638 . . 3  |-  ( F  Fn  V  <->  F : V -onto-> ran  F )
97, 8sylib 196 . 2  |-  ( ph  ->  F : V -onto-> ran  F )
105rnmpt 5097 . . . 4  |-  ran  F  =  { y  |  E. x  e.  V  y  =  [ x ]  .~  }
11 df-qs 7119 . . . 4  |-  ( V /.  .~  )  =  { y  |  E. x  e.  V  y  =  [ x ]  .~  }
1210, 11eqtr4i 2466 . . 3  |-  ran  F  =  ( V /.  .~  )
13 foeq3 5630 . . 3  |-  ( ran 
F  =  ( V /.  .~  )  -> 
( F : V -onto-> ran  F  <->  F : V -onto-> ( V /.  .~  ) ) )
1412, 13ax-mp 5 . 2  |-  ( F : V -onto-> ran  F  <->  F : V -onto-> ( V /.  .~  ) )
159, 14sylib 196 1  |-  ( ph  ->  F : V -onto-> ( V /.  .~  ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2727   E.wrex 2728   _Vcvv 2984    e. cmpt 4362   ran crn 4853    Fn wfn 5425   -onto->wfo 5428   ` cfv 5430  (class class class)co 6103   [cec 7111   /.cqs 7112   Basecbs 14186    /.s cqus 14455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-fun 5432  df-fn 5433  df-fo 5436  df-ec 7115  df-qs 7119
This theorem is referenced by:  divsbas  14495  divssca  14496  divsaddvallem  14501  divsaddflem  14502  divsaddval  14503  divsaddf  14504  divsmulval  14505  divsmulf  14506  divsgrp2  15685  divsrng2  16724  znzrhfo  17992  divstps  19307  divstgpopn  19702  divstgplem  19703  divstgphaus  19705
  Copyright terms: Public domain W3C validator