Theorem ffnfv 7061

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 6659	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7023	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3126	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6891	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3258	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3222	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2821	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3241	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3937	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6493	. . 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 3049  ∃wrex 3058   ⊆ wss 3899  ran crn 5622   Fn wfn 6484  ⟶wf 6485  ‘cfv 6489

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497

This theorem is referenced by:  ffnfvf  7062  fnfvrnss  7063  fcdmssb  7064  fmpt2d  7066  fssrescdmd  7068  fconstfv  7155  ffnov  7481  seqomlem2  8379  naddf  8605  elixpconst  8838  elixpsn  8870  unblem4  9189  ordtypelem4  9417  oismo  9436  cantnfvalf  9565  rankf  9697  alephon  9970  alephf1  9986  alephf1ALT  10004  alephfplem4  10008  cfsmolem  10171  infpssrlem3  10206  axcc4  10340  domtriomlem  10343  pwfseqlem3  10561  gch3  10577  inar1  10676  peano5nni  12138  cnref1o  12893  seqf2  13938  hashkf  14249  iswrdsymb  14448  ccatrn  14507  shftf  14996  sqrtf  15281  isercoll2  15586  eff2  16018  reeff1  16039  1arith  16849  ramcl  16951  xpscf  17479  dmaf  17966  cdaf  17967  coapm  17988  odf  19459  gsumpt  19884  dprdff  19936  dprdfcntz  19939  dprdfadd  19944  dprdlub  19950  rngmgpf  20085  mgpf  20176  prdscrngd  20250  isabvd  20737  psgnghm  21527  frlmsslsp  21743  psrbagcon  21872  mvrf2  21940  subrgmvrf  21979  mplbas2  21987  kqf  23672  fmf  23870  tmdgsum2  24021  prdstmdd  24049  prdstgpd  24050  prdsxmslem2  24454  metdsre  24779  evth  24895  evthicc2  25398  ovolfsf  25409  ovolf  25420  vitalilem2  25547  vitalilem5  25550  0plef  25610  mbfi1fseqlem4  25656  xrge0f  25669  itg2addlem  25696  dvfre  25892  dvne0  25953  mdegxrf  26010  mtest  26350  psercn  26373  recosf1o  26481  logcn  26593  amgm  26938  emcllem7  26949  dchrfi  27203  dchr1re  27211  dchrisum0re  27461  padicabvf  27579  addsf  27935  negsf  28004  noseqind  28232  vtxdgfisf  29466  hlimf  31228  pjrni  31693  pjmf1  31707  2ndresdju  32642  nsgmgc  33388  mplvrpmrhm  33588  reprinfz1  34646  reprdifc  34651  bnj149  34898  subfacp1lem3  35237  mrsubrn  35568  msrf  35597  mclsind  35625  neibastop2lem  36415  weiunlem2  36518  rrncmslem  37882  cdlemk56  41080  sticksstones22  42271  hbtlem7  43232  dgraaf  43254  deg1mhm  43307  elixpconstg  45200  elmapsnd  45315  unirnmap  45319  resincncf  45987  dvnprodlem1  46058  volioof  46099  voliooicof  46108  qndenserrnbllem  46406  subsaliuncllem  46469  fge0iccico  46482  elhoi  46654  ovnsubaddlem1  46682  hoiqssbllem3  46736  ovolval4lem1  46761  rrx2xpref1o  48833  oppff1  49263  fucofulem2  49426