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

Theorem ffnfv 5897
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 5594 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 ffvelrn 5871 . . . 4  |-  ( ( F : A --> B  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
32ralrimiva 2791 . . 3  |-  ( F : A --> B  ->  A. x  e.  A  ( F `  x )  e.  B )
41, 3jca 520 . 2  |-  ( F : A --> B  -> 
( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
5 simpl 445 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F  Fn  A )
6 fvelrnb 5777 . . . . . 6  |-  ( F  Fn  A  ->  (
y  e.  ran  F  <->  E. x  e.  A  ( F `  x )  =  y ) )
76biimpd 200 . . . . 5  |-  ( F  Fn  A  ->  (
y  e.  ran  F  ->  E. x  e.  A  ( F `  x )  =  y ) )
8 nfra1 2758 . . . . . 6  |-  F/ x A. x  e.  A  ( F `  x )  e.  B
9 nfv 1630 . . . . . 6  |-  F/ x  y  e.  B
10 rsp 2768 . . . . . . 7  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  ( F `  x )  e.  B ) )
11 eleq1 2498 . . . . . . . 8  |-  ( ( F `  x )  =  y  ->  (
( F `  x
)  e.  B  <->  y  e.  B ) )
1211biimpcd 217 . . . . . . 7  |-  ( ( F `  x )  e.  B  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) )
1310, 12syl6 32 . . . . . 6  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  (
( F `  x
)  =  y  -> 
y  e.  B ) ) )
148, 9, 13rexlimd 2829 . . . . 5  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( E. x  e.  A  ( F `  x )  =  y  ->  y  e.  B ) )
157, 14sylan9 640 . . . 4  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  -> 
( y  e.  ran  F  ->  y  e.  B
) )
1615ssrdv 3356 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  ran  F  C_  B )
17 df-f 5461 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
185, 16, 17sylanbrc 647 . 2  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  F : A --> B )
194, 18impbii 182 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 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707   E.wrex 2708    C_ wss 3322   ran crn 4882    Fn wfn 5452   -->wf 5453   ` cfv 5457
This theorem is referenced by:  ffnfvf  5898  fnfvrnss  5899  fmpt2d  5901  ffnov  6177  seqomlem2  6711  abianfp  6719  elixpconst  7073  elixpsn  7104  unblem4  7365  ordtypelem4  7493  oismo  7512  cantnfvalf  7623  rankf  7723  alephon  7955  alephf1  7971  alephf1ALT  7989  alephfplem4  7993  cfsmolem  8155  infpssrlem3  8190  axcc4  8324  domtriomlem  8327  axdclem2  8405  pwfseqlem3  8540  gch3  8556  inar1  8655  peano5nni  10008  cnref1o  10612  seqf2  11347  hashkf  11625  shftf  11899  sqrf  12172  isercoll2  12467  eff2  12705  reeff1  12726  1arith  13300  ramcl  13402  xpscf  13796  dmaf  14209  cdaf  14210  coapm  14231  odf  15180  gsumpt  15550  dprdff  15575  dprdfcntz  15578  dprdfadd  15583  dprdlub  15589  mgpf  15680  prdscrngd  15724  isabvd  15913  psrbagcon  16441  subrgmvrf  16530  mplbas2  16536  mvrf2  16557  kqf  17784  fmf  17982  tmdgsum2  18131  prdstmdd  18158  prdstgpd  18159  prdsxmslem2  18564  metdsre  18888  evth  18989  evthicc2  19362  ovolfsf  19373  ovolf  19383  vitalilem2  19506  vitalilem5  19509  0plef  19567  mbfi1fseqlem4  19613  xrge0f  19626  itg2addlem  19653  dvfre  19842  dvne0  19900  mdegxrf  19996  mtest  20325  psercn  20347  recosf1o  20442  logcn  20543  amgm  20834  emcllem7  20845  dchrfi  21044  dchr1re  21052  dchrisum0re  21212  padicabvf  21330  hlimf  22745  pjrni  23209  pjmf1  23223  subfacp1lem3  24873  neibastop2lem  26403  rrncmslem  26555  frlmsslsp  27239  hbtlem7  27320  dgraaf  27343  psgnghm  27428  deg1mhm  27517  bnj149  29320  cdlemk56  31842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465
  Copyright terms: Public domain W3C validator