Theorem ffnfv 7066

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 6663	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7028	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3130	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6895	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3226	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2825	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 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 3928	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6497	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 584	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 209	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3890  ran crn 5626   Fn wfn 6488  ⟶wf 6489  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501

This theorem is referenced by:  ffnfvf  7067  fnfvrnss  7068  fcdmssb  7069  fmpt2d  7072  fssrescdmd  7074  fconstfv  7161  ffnov  7487  seqomlem2  8384  naddf  8611  elixpconst  8847  elixpsn  8879  unblem4  9199  ordtypelem4  9430  oismo  9449  cantnfvalf  9580  rankf  9712  alephon  9985  alephf1  10001  alephf1ALT  10019  alephfplem4  10023  cfsmolem  10186  infpssrlem3  10221  axcc4  10355  domtriomlem  10358  pwfseqlem3  10577  gch3  10593  inar1  10692  peano5nni  12171  cnref1o  12929  seqf2  13977  hashkf  14288  iswrdsymb  14487  ccatrn  14546  shftf  15035  sqrtf  15320  isercoll2  15625  eff2  16060  reeff1  16081  1arith  16892  ramcl  16994  xpscf  17523  dmaf  18010  cdaf  18011  coapm  18032  odf  19506  gsumpt  19931  dprdff  19983  dprdfcntz  19986  dprdfadd  19991  dprdlub  19997  rngmgpf  20132  mgpf  20223  prdscrngd  20295  isabvd  20783  psgnghm  21573  frlmsslsp  21789  psrbagcon  21918  mvrf2  21984  subrgmvrf  22025  mplbas2  22033  kqf  23725  fmf  23923  tmdgsum2  24074  prdstmdd  24102  prdstgpd  24103  prdsxmslem2  24507  metdsre  24832  evth  24939  evthicc2  25440  ovolfsf  25451  ovolf  25462  vitalilem2  25589  vitalilem5  25592  0plef  25652  mbfi1fseqlem4  25698  xrge0f  25711  itg2addlem  25738  dvfre  25931  dvne0  25991  mdegxrf  26046  mtest  26385  psercn  26407  recosf1o  26515  logcn  26627  amgm  26971  emcllem7  26982  dchrfi  27235  dchr1re  27243  dchrisum0re  27493  padicabvf  27611  addsf  27991  negsf  28061  noseqind  28301  vtxdgfisf  29563  hlimf  31326  pjrni  31791  pjmf1  31805  2ndresdju  32740  nsgmgc  33490  mplvrpmrhm  33709  reprinfz1  34785  reprdifc  34790  bnj149  35036  subfacp1lem3  35383  mrsubrn  35714  msrf  35743  mclsind  35771  neibastop2lem  36561  weiunlem  36664  mh-inf3f1  36742  rrncmslem  38170  cdlemk56  41434  sticksstones22  42624  hbtlem7  43574  dgraaf  43596  deg1mhm  43649  elixpconstg  45540  elmapsnd  45654  unirnmap  45658  resincncf  46324  dvnprodlem1  46395  volioof  46436  voliooicof  46445  qndenserrnbllem  46743  subsaliuncllem  46806  fge0iccico  46819  elhoi  46991  ovnsubaddlem1  47019  hoiqssbllem3  47073  ovolval4lem1  47098  rrx2xpref1o  49209  oppff1  49638  fucofulem2  49801