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.

Step	Hyp	Ref	Expression
1		ffn 6668	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7033	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3129	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6900	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3261	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3225	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2824	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3244	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3927	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6502	. . 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 3051  ∃wrex 3061   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  ffnfvf  7072  fnfvrnss  7073  fcdmssb  7074  fmpt2d  7077  fssrescdmd  7079  fconstfv  7167  ffnov  7493  seqomlem2  8390  naddf  8617  elixpconst  8853  elixpsn  8885  unblem4  9205  ordtypelem4  9436  oismo  9455  cantnfvalf  9586  rankf  9718  alephon  9991  alephf1  10007  alephf1ALT  10025  alephfplem4  10029  cfsmolem  10192  infpssrlem3  10227  axcc4  10361  domtriomlem  10364  pwfseqlem3  10583  gch3  10599  inar1  10698  peano5nni  12177  cnref1o  12935  seqf2  13983  hashkf  14294  iswrdsymb  14493  ccatrn  14552  shftf  15041  sqrtf  15326  isercoll2  15631  eff2  16066  reeff1  16087  1arith  16898  ramcl  17000  xpscf  17529  dmaf  18016  cdaf  18017  coapm  18038  odf  19512  gsumpt  19937  dprdff  19989  dprdfcntz  19992  dprdfadd  19997  dprdlub  20003  rngmgpf  20138  mgpf  20229  prdscrngd  20301  isabvd  20789  psgnghm  21560  frlmsslsp  21776  psrbagcon  21905  mvrf2  21971  subrgmvrf  22012  mplbas2  22020  kqf  23712  fmf  23910  tmdgsum2  24061  prdstmdd  24089  prdstgpd  24090  prdsxmslem2  24494  metdsre  24819  evth  24926  evthicc2  25427  ovolfsf  25438  ovolf  25449  vitalilem2  25576  vitalilem5  25579  0plef  25639  mbfi1fseqlem4  25685  xrge0f  25698  itg2addlem  25725  dvfre  25918  dvne0  25978  mdegxrf  26033  mtest  26369  psercn  26391  recosf1o  26499  logcn  26611  amgm  26954  emcllem7  26965  dchrfi  27218  dchr1re  27226  dchrisum0re  27476  padicabvf  27594  addsf  27974  negsf  28044  noseqind  28284  vtxdgfisf  29545  hlimf  31308  pjrni  31773  pjmf1  31787  2ndresdju  32722  nsgmgc  33472  mplvrpmrhm  33691  reprinfz1  34766  reprdifc  34771  bnj149  35017  subfacp1lem3  35364  mrsubrn  35695  msrf  35724  mclsind  35752  neibastop2lem  36542  weiunlem  36645  mh-inf3f1  36723  rrncmslem  38153  cdlemk56  41417  sticksstones22  42607  hbtlem7  43553  dgraaf  43575  deg1mhm  43628  elixpconstg  45519  elmapsnd  45633  unirnmap  45637  resincncf  46303  dvnprodlem1  46374  volioof  46415  voliooicof  46424  qndenserrnbllem  46722  subsaliuncllem  46785  fge0iccico  46798  elhoi  46970  ovnsubaddlem1  46998  hoiqssbllem3  47052  ovolval4lem1  47077  rrx2xpref1o  49194  oppff1  49623  fucofulem2  49786