Theorem ffnfv 7064

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 6662	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7026	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3128	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6894	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3260	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3224	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2824	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3243	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3939	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 583	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 209	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  ffnfvf  7065  fnfvrnss  7066  fcdmssb  7067  fmpt2d  7069  fssrescdmd  7071  fconstfv  7158  ffnov  7484  seqomlem2  8382  naddf  8609  elixpconst  8845  elixpsn  8877  unblem4  9197  ordtypelem4  9428  oismo  9447  cantnfvalf  9576  rankf  9708  alephon  9981  alephf1  9997  alephf1ALT  10015  alephfplem4  10019  cfsmolem  10182  infpssrlem3  10217  axcc4  10351  domtriomlem  10354  pwfseqlem3  10573  gch3  10589  inar1  10688  peano5nni  12150  cnref1o  12900  seqf2  13946  hashkf  14257  iswrdsymb  14456  ccatrn  14515  shftf  15004  sqrtf  15289  isercoll2  15594  eff2  16026  reeff1  16047  1arith  16857  ramcl  16959  xpscf  17488  dmaf  17975  cdaf  17976  coapm  17997  odf  19468  gsumpt  19893  dprdff  19945  dprdfcntz  19948  dprdfadd  19953  dprdlub  19959  rngmgpf  20094  mgpf  20185  prdscrngd  20259  isabvd  20747  psgnghm  21537  frlmsslsp  21753  psrbagcon  21883  mvrf2  21950  subrgmvrf  21991  mplbas2  21999  kqf  23693  fmf  23891  tmdgsum2  24042  prdstmdd  24070  prdstgpd  24071  prdsxmslem2  24475  metdsre  24800  evth  24916  evthicc2  25419  ovolfsf  25430  ovolf  25441  vitalilem2  25568  vitalilem5  25571  0plef  25631  mbfi1fseqlem4  25677  xrge0f  25690  itg2addlem  25717  dvfre  25913  dvne0  25974  mdegxrf  26031  mtest  26371  psercn  26394  recosf1o  26502  logcn  26614  amgm  26959  emcllem7  26970  dchrfi  27224  dchr1re  27232  dchrisum0re  27482  padicabvf  27600  addsf  27980  negsf  28050  noseqind  28290  vtxdgfisf  29552  hlimf  31314  pjrni  31779  pjmf1  31793  2ndresdju  32729  nsgmgc  33495  mplvrpmrhm  33714  reprinfz1  34781  reprdifc  34786  bnj149  35033  subfacp1lem3  35378  mrsubrn  35709  msrf  35738  mclsind  35766  neibastop2lem  36556  weiunlem  36659  rrncmslem  38035  cdlemk56  41253  sticksstones22  42444  hbtlem7  43388  dgraaf  43410  deg1mhm  43463  elixpconstg  45354  elmapsnd  45469  unirnmap  45473  resincncf  46140  dvnprodlem1  46211  volioof  46252  voliooicof  46261  qndenserrnbllem  46559  subsaliuncllem  46622  fge0iccico  46635  elhoi  46807  ovnsubaddlem1  46835  hoiqssbllem3  46889  ovolval4lem1  46914  rrx2xpref1o  48985  oppff1  49414  fucofulem2  49577