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

Theorem ffnfv 5861
Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
Assertion
Ref Expression
ffnfv  |-  ( F : A --> B  <->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B
) )
Distinct variable groups:    x, A    x, B    x, F

Proof of Theorem ffnfv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ffn 5558 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 ffvelrn 5835 . . . 4  |-  ( ( F : A --> B  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
32ralrimiva 2757 . . 3  |-  ( F : A --> B  ->  A. x  e.  A  ( F `  x )  e.  B )
41, 3jca 519 . 2  |-  ( F : A --> B  -> 
( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
5 simpl 444 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F  Fn  A )
6 fvelrnb 5741 . . . . . 6  |-  ( F  Fn  A  ->  (
y  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  y ) )
76biimpd 199 . . . . 5  |-  ( F  Fn  A  ->  (
y  e.  ran  F  ->  E. x  e.  A  ( F `  x )  =  y ) )
8 nfra1 2724 . . . . . 6  |-  F/ x A. x  e.  A  ( F `  x )  e.  B
9 nfv 1626 . . . . . 6  |-  F/ x  y  e.  B
10 rsp 2734 . . . . . . 7  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  ( F `  x )  e.  B ) )
11 eleq1 2472 . . . . . . . 8  |-  ( ( F `  x )  =  y  ->  (
( F `  x
)  e.  B  <->  y  e.  B ) )
1211biimpcd 216 . . . . . . 7  |-  ( ( F `  x )  e.  B  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) )
1310, 12syl6 31 . . . . . 6  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) ) )
148, 9, 13rexlimd 2795 . . . . 5  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( E. x  e.  A  ( F `  x )  =  y  ->  y  e.  B ) )
157, 14sylan9 639 . . . 4  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  -> 
( y  e.  ran  F  ->  y  e.  B
) )
1615ssrdv 3322 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  ran  F  C_  B )
17 df-f 5425 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
185, 16, 17sylanbrc 646 . 2  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F : A --> B )
194, 18impbii 181 1  |-  ( F : A --> B  <->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2674   E.wrex 2675    C_ wss 3288   ran crn 4846    Fn wfn 5416   -->wf 5417   ` cfv 5421
This theorem is referenced by:  ffnfvf  5862  fnfvrnss  5863  fmpt2d  5865  ffnov  6141  seqomlem2  6675  abianfp  6683  elixpconst  7037  elixpsn  7068  unblem4  7329  ordtypelem4  7454  oismo  7473  cantnfvalf  7584  rankf  7684  alephon  7914  alephf1  7930  alephf1ALT  7948  alephfplem4  7952  cfsmolem  8114  infpssrlem3  8149  axcc4  8283  domtriomlem  8286  axdclem2  8364  pwfseqlem3  8499  gch3  8519  inar1  8614  peano5nni  9967  cnref1o  10571  seqf2  11305  hashkf  11583  shftf  11857  sqrf  12130  isercoll2  12425  eff2  12663  reeff1  12684  1arith  13258  ramcl  13360  xpscf  13754  dmaf  14167  cdaf  14168  coapm  14189  odf  15138  gsumpt  15508  dprdff  15533  dprdfcntz  15536  dprdfadd  15541  dprdlub  15547  mgpf  15638  prdscrngd  15682  isabvd  15871  psrbagcon  16399  subrgmvrf  16488  mplbas2  16494  mvrf2  16515  kqf  17740  fmf  17938  tmdgsum2  18087  prdstmdd  18114  prdstgpd  18115  prdsxmslem2  18520  metdsre  18844  evth  18945  evthicc2  19318  ovolfsf  19329  ovolf  19339  vitalilem2  19462  vitalilem5  19465  0plef  19525  mbfi1fseqlem4  19571  xrge0f  19584  itg2addlem  19611  dvfre  19798  dvne0  19856  mdegxrf  19952  mtest  20281  psercn  20303  recosf1o  20398  logcn  20499  amgm  20790  emcllem7  20801  dchrfi  21000  dchr1re  21008  dchrisum0re  21168  padicabvf  21286  hlimf  22701  pjrni  23165  pjmf1  23179  subfacp1lem3  24829  neibastop2lem  26287  rrncmslem  26439  frlmsslsp  27124  hbtlem7  27205  dgraaf  27228  psgnghm  27313  deg1mhm  27402  bnj149  28964  cdlemk56  31465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429
  Copyright terms: Public domain W3C validator