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

Theorem ffnfv 7071
Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
Assertion
Ref Expression
ffnfv (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem ffnfv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ffn 6673 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 ffvelcdm 7037 . . . 4 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
32ralrimiva 3144 . . 3 (𝐹:𝐴𝐵 → ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)
41, 3jca 513 . 2 (𝐹:𝐴𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
5 simpl 484 . . 3 ((𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6 fvelrnb 6908 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝑦))
76biimpd 228 . . . . 5 (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥𝐴 (𝐹𝑥) = 𝑦))
8 nfra1 3270 . . . . . 6 𝑥𝑥𝐴 (𝐹𝑥) ∈ 𝐵
9 nfv 1918 . . . . . 6 𝑥 𝑦𝐵
10 rsp 3233 . . . . . . 7 (∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵 → (𝑥𝐴 → (𝐹𝑥) ∈ 𝐵))
11 eleq1 2826 . . . . . . . 8 ((𝐹𝑥) = 𝑦 → ((𝐹𝑥) ∈ 𝐵𝑦𝐵))
1211biimpcd 249 . . . . . . 7 ((𝐹𝑥) ∈ 𝐵 → ((𝐹𝑥) = 𝑦𝑦𝐵))
1310, 12syl6 35 . . . . . 6 (∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵 → (𝑥𝐴 → ((𝐹𝑥) = 𝑦𝑦𝐵)))
148, 9, 13rexlimd 3252 . . . . 5 (∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵 → (∃𝑥𝐴 (𝐹𝑥) = 𝑦𝑦𝐵))
157, 14sylan9 509 . . . 4 ((𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹𝑦𝐵))
1615ssrdv 3955 . . 3 ((𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) → ran 𝐹𝐵)
17 df-f 6505 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
185, 16, 17sylanbrc 584 . 2 ((𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) → 𝐹:𝐴𝐵)
194, 18impbii 208 1 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3065  wrex 3074  wss 3915  ran crn 5639   Fn wfn 6496  wf 6497  cfv 6501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509
This theorem is referenced by:  ffnfvf  7072  fnfvrnss  7073  fcdmssb  7074  fmpt2d  7076  fconstfv  7167  ffnov  7488  seqomlem2  8402  naddf  8632  elixpconst  8850  elixpsn  8882  unblem4  9249  ordtypelem4  9464  oismo  9483  cantnfvalf  9608  rankf  9737  alephon  10012  alephf1  10028  alephf1ALT  10046  alephfplem4  10050  cfsmolem  10213  infpssrlem3  10248  axcc4  10382  domtriomlem  10385  pwfseqlem3  10603  gch3  10619  inar1  10718  peano5nni  12163  cnref1o  12917  seqf2  13934  hashkf  14239  iswrdsymb  14426  ccatrn  14484  shftf  14971  sqrtf  15255  isercoll2  15560  eff2  15988  reeff1  16009  1arith  16806  ramcl  16908  xpscf  17454  dmaf  17942  cdaf  17943  coapm  17964  odf  19326  gsumpt  19746  dprdff  19798  dprdfcntz  19801  dprdfadd  19806  dprdlub  19812  mgpf  19986  prdscrngd  20044  isabvd  20295  psgnghm  21000  frlmsslsp  21218  psrbagcon  21348  psrbagconOLD  21349  subrgmvrf  21451  mplbas2  21459  mvrf2  21484  kqf  23114  fmf  23312  tmdgsum2  23463  prdstmdd  23491  prdstgpd  23492  prdsxmslem2  23901  metdsre  24232  evth  24338  evthicc2  24840  ovolfsf  24851  ovolf  24862  vitalilem2  24989  vitalilem5  24992  0plef  25052  mbfi1fseqlem4  25099  xrge0f  25112  itg2addlem  25139  dvfre  25331  dvne0  25391  mdegxrf  25449  mtest  25779  psercn  25801  recosf1o  25907  logcn  26018  amgm  26356  emcllem7  26367  dchrfi  26619  dchr1re  26627  dchrisum0re  26877  padicabvf  26995  addsf  27314  negsf  27369  vtxdgfisf  28466  hlimf  30221  pjrni  30686  pjmf1  30700  2ndresdju  31607  nsgmgc  32230  reprinfz1  33275  reprdifc  33280  bnj149  33527  subfacp1lem3  33816  mrsubrn  34147  msrf  34176  mclsind  34204  neibastop2lem  34861  rrncmslem  36320  cdlemk56  39463  sticksstones22  40605  hbtlem7  41481  dgraaf  41503  deg1mhm  41563  elixpconstg  43373  elmapsnd  43499  unirnmap  43503  resincncf  44190  dvnprodlem1  44261  volioof  44302  voliooicof  44311  qndenserrnbllem  44609  subsaliuncllem  44672  fge0iccico  44685  elhoi  44857  ovnsubaddlem1  44885  hoiqssbllem3  44939  ovolval4lem1  44964  rrx2xpref1o  46878
  Copyright terms: Public domain W3C validator