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

Theorem ffnfv 5894
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 5591 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 ffvelrn 5868 . . . 4  |-  ( ( F : A --> B  /\  x  e.  A )  ->  ( F `  x
)  e.  B )
32ralrimiva 2789 . . 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 5774 . . . . . 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 2756 . . . . . 6  |-  F/ x A. x  e.  A  ( F `  x )  e.  B
9 nfv 1629 . . . . . 6  |-  F/ x  y  e.  B
10 rsp 2766 . . . . . . 7  |-  ( A. x  e.  A  ( F `  x )  e.  B  ->  ( x  e.  A  ->  ( F `  x )  e.  B ) )
11 eleq1 2496 . . . . . . . 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 2827 . . . . 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 3354 . . 3  |-  ( ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  ->  ran  F  C_  B )
17 df-f 5458 . . 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 1652    e. wcel 1725   A.wral 2705   E.wrex 2706    C_ wss 3320   ran crn 4879    Fn wfn 5449   -->wf 5450   ` cfv 5454
This theorem is referenced by:  ffnfvf  5895  fnfvrnss  5896  fmpt2d  5898  ffnov  6174  seqomlem2  6708  abianfp  6716  elixpconst  7070  elixpsn  7101  unblem4  7362  ordtypelem4  7490  oismo  7509  cantnfvalf  7620  rankf  7720  alephon  7950  alephf1  7966  alephf1ALT  7984  alephfplem4  7988  cfsmolem  8150  infpssrlem3  8185  axcc4  8319  domtriomlem  8322  axdclem2  8400  pwfseqlem3  8535  gch3  8555  inar1  8650  peano5nni  10003  cnref1o  10607  seqf2  11342  hashkf  11620  shftf  11894  sqrf  12167  isercoll2  12462  eff2  12700  reeff1  12721  1arith  13295  ramcl  13397  xpscf  13791  dmaf  14204  cdaf  14205  coapm  14226  odf  15175  gsumpt  15545  dprdff  15570  dprdfcntz  15573  dprdfadd  15578  dprdlub  15584  mgpf  15675  prdscrngd  15719  isabvd  15908  psrbagcon  16436  subrgmvrf  16525  mplbas2  16531  mvrf2  16552  kqf  17779  fmf  17977  tmdgsum2  18126  prdstmdd  18153  prdstgpd  18154  prdsxmslem2  18559  metdsre  18883  evth  18984  evthicc2  19357  ovolfsf  19368  ovolf  19378  vitalilem2  19501  vitalilem5  19504  0plef  19564  mbfi1fseqlem4  19610  xrge0f  19623  itg2addlem  19650  dvfre  19837  dvne0  19895  mdegxrf  19991  mtest  20320  psercn  20342  recosf1o  20437  logcn  20538  amgm  20829  emcllem7  20840  dchrfi  21039  dchr1re  21047  dchrisum0re  21207  padicabvf  21325  hlimf  22740  pjrni  23204  pjmf1  23218  subfacp1lem3  24868  neibastop2lem  26389  rrncmslem  26541  frlmsslsp  27225  hbtlem7  27306  dgraaf  27329  psgnghm  27414  deg1mhm  27503  bnj149  29246  cdlemk56  31768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-fv 5462
  Copyright terms: Public domain W3C validator