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

Theorem ffnfv 5796
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 5495 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 ffvelrn 5770 . . . 4  |-  ( ( F : A --> B  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
32ralrimiva 2711 . . 3  |-  ( F : A --> B  ->  A. x  e.  A  ( F `  x )  e.  B )
41, 3jca 518 . 2  |-  ( F : A --> B  -> 
( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
5 simpl 443 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F  Fn  A )
6 fvelrnb 5677 . . . . . 6  |-  ( F  Fn  A  ->  (
y  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  y ) )
76biimpd 198 . . . . 5  |-  ( F  Fn  A  ->  (
y  e.  ran  F  ->  E. x  e.  A  ( F `  x )  =  y ) )
8 nfra1 2678 . . . . . 6  |-  F/ x A. x  e.  A  ( F `  x )  e.  B
9 nfv 1624 . . . . . 6  |-  F/ x  y  e.  B
10 rsp 2688 . . . . . . 7  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  ( F `  x )  e.  B ) )
11 eleq1 2426 . . . . . . . 8  |-  ( ( F `  x )  =  y  ->  (
( F `  x
)  e.  B  <->  y  e.  B ) )
1211biimpcd 215 . . . . . . 7  |-  ( ( F `  x )  e.  B  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) )
1310, 12syl6 29 . . . . . 6  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) ) )
148, 9, 13rexlimd 2749 . . . . 5  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( E. x  e.  A  ( F `  x )  =  y  ->  y  e.  B ) )
157, 14sylan9 638 . . . 4  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  -> 
( y  e.  ran  F  ->  y  e.  B
) )
1615ssrdv 3271 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  ran  F  C_  B )
17 df-f 5362 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
185, 16, 17sylanbrc 645 . 2  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F : A --> B )
194, 18impbii 180 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 176    /\ wa 358    = wceq 1647    e. wcel 1715   A.wral 2628   E.wrex 2629    C_ wss 3238   ran crn 4793    Fn wfn 5353   -->wf 5354   ` cfv 5358
This theorem is referenced by:  ffnfvf  5797  fnfvrnss  5798  fmpt2d  5799  ffnov  6074  seqomlem2  6605  abianfp  6613  elixpconst  6967  elixpsn  6998  unblem4  7259  ordtypelem4  7383  oismo  7402  cantnfvalf  7513  rankf  7613  alephon  7843  alephf1  7859  alephf1ALT  7877  alephfplem4  7881  cfsmolem  8043  infpssrlem3  8078  axcc4  8212  domtriomlem  8215  axdclem2  8294  pwfseqlem3  8429  gch3  8449  inar1  8544  peano5nni  9896  cnref1o  10500  seqf2  11229  hashkf  11507  shftf  11781  sqrf  12054  isercoll2  12349  eff2  12587  reeff1  12608  1arith  13182  ramcl  13284  xpscf  13678  dmaf  14091  cdaf  14092  coapm  14113  odf  15062  gsumpt  15432  dprdff  15457  dprdfcntz  15460  dprdfadd  15465  dprdlub  15471  mgpf  15562  prdscrngd  15606  isabvd  15795  psrbagcon  16327  subrgmvrf  16416  mplbas2  16422  mvrf2  16443  kqf  17655  fmf  17853  tmdgsum2  17992  prdstmdd  18019  prdstgpd  18020  prdsxmslem2  18288  metdsre  18571  evth  18672  evthicc2  19035  ovolfsf  19046  ovolf  19056  vitalilem2  19179  vitalilem5  19182  0plef  19242  mbfi1fseqlem4  19288  xrge0f  19301  itg2addlem  19328  dvfre  19515  dvne0  19573  mdegxrf  19669  mtest  19998  psercn  20020  recosf1o  20115  logcn  20216  amgm  20507  emcllem7  20518  dchrfi  20717  dchr1re  20725  dchrisum0re  20885  padicabvf  21003  hlimf  22130  pjrni  22594  pjmf1  22608  ofcfval4  23953  subfacp1lem3  24316  neibastop2lem  25816  rrncmslem  26062  frlmsslsp  26754  hbtlem7  26835  dgraaf  26858  psgnghm  26943  deg1mhm  27032  stoweidlem31  27286  bnj149  28671  cdlemk56  31231
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pr 4316
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-fv 5366
  Copyright terms: Public domain W3C validator