Theorem ffnfv 6974

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.

Step	Hyp	Ref	Expression
1		ffn 6584	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6941	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3107	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6812	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 228	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3142	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3129	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2826	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 248	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3245	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3923	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6422	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 582	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 208	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426

This theorem is referenced by:  ffnfvf  6975  fnfvrnss  6976  frnssb  6977  fmpt2d  6979  fconstfv  7070  ffnov  7379  seqomlem2  8252  elixpconst  8651  elixpsn  8683  unblem4  8999  ordtypelem4  9210  oismo  9229  cantnfvalf  9353  rankf  9483  alephon  9756  alephf1  9772  alephf1ALT  9790  alephfplem4  9794  cfsmolem  9957  infpssrlem3  9992  axcc4  10126  domtriomlem  10129  pwfseqlem3  10347  gch3  10363  inar1  10462  peano5nni  11906  cnref1o  12654  seqf2  13670  hashkf  13974  iswrdsymb  14162  ccatrn  14222  shftf  14718  sqrtf  15003  isercoll2  15308  eff2  15736  reeff1  15757  1arith  16556  ramcl  16658  xpscf  17193  dmaf  17680  cdaf  17681  coapm  17702  odf  19060  gsumpt  19478  dprdff  19530  dprdfcntz  19533  dprdfadd  19538  dprdlub  19544  mgpf  19713  prdscrngd  19767  isabvd  19995  psgnghm  20697  frlmsslsp  20913  psrbagcon  21043  psrbagconOLD  21044  subrgmvrf  21145  mplbas2  21153  mvrf2  21178  kqf  22806  fmf  23004  tmdgsum2  23155  prdstmdd  23183  prdstgpd  23184  prdsxmslem2  23591  metdsre  23922  evth  24028  evthicc2  24529  ovolfsf  24540  ovolf  24551  vitalilem2  24678  vitalilem5  24681  0plef  24741  mbfi1fseqlem4  24788  xrge0f  24801  itg2addlem  24828  dvfre  25020  dvne0  25080  mdegxrf  25138  mtest  25468  psercn  25490  recosf1o  25596  logcn  25707  amgm  26045  emcllem7  26056  dchrfi  26308  dchr1re  26316  dchrisum0re  26566  padicabvf  26684  vtxdgfisf  27746  hlimf  29500  pjrni  29965  pjmf1  29979  2ndresdju  30887  nsgmgc  31499  reprinfz1  32502  reprdifc  32507  bnj149  32755  subfacp1lem3  33044  mrsubrn  33375  msrf  33404  mclsind  33432  neibastop2lem  34476  rrncmslem  35917  cdlemk56  38912  sticksstones22  40052  hbtlem7  40866  dgraaf  40888  deg1mhm  40948  elixpconstg  42528  elmapsnd  42633  unirnmap  42637  resincncf  43306  dvnprodlem1  43377  volioof  43418  voliooicof  43427  qndenserrnbllem  43725  subsaliuncllem  43786  fge0iccico  43798  elhoi  43970  ovnsubaddlem1  43998  hoiqssbllem3  44052  ovolval4lem1  44077  rrx2xpref1o  45952