Theorem ffnfv 7062

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 6660	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7024	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3126	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6892	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3258	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3222	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2822	. . . . . . . 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 6494	. . 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 5623   Fn wfn 6485  ⟶wf 6486  ‘cfv 6490

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 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2567  df-clab 2713  df-cleq 2726  df-clel 2809  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 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498

This theorem is referenced by:  ffnfvf  7063  fnfvrnss  7064  fcdmssb  7065  fmpt2d  7067  fssrescdmd  7069  fconstfv  7156  ffnov  7482  seqomlem2  8380  naddf  8607  elixpconst  8841  elixpsn  8873  unblem4  9193  ordtypelem4  9424  oismo  9443  cantnfvalf  9572  rankf  9704  alephon  9977  alephf1  9993  alephf1ALT  10011  alephfplem4  10015  cfsmolem  10178  infpssrlem3  10213  axcc4  10347  domtriomlem  10350  pwfseqlem3  10569  gch3  10585  inar1  10684  peano5nni  12146  cnref1o  12896  seqf2  13942  hashkf  14253  iswrdsymb  14452  ccatrn  14511  shftf  15000  sqrtf  15285  isercoll2  15590  eff2  16022  reeff1  16043  1arith  16853  ramcl  16955  xpscf  17484  dmaf  17971  cdaf  17972  coapm  17993  odf  19464  gsumpt  19889  dprdff  19941  dprdfcntz  19944  dprdfadd  19949  dprdlub  19955  rngmgpf  20090  mgpf  20181  prdscrngd  20255  isabvd  20743  psgnghm  21533  frlmsslsp  21749  psrbagcon  21879  mvrf2  21946  subrgmvrf  21987  mplbas2  21995  kqf  23689  fmf  23887  tmdgsum2  24038  prdstmdd  24066  prdstgpd  24067  prdsxmslem2  24471  metdsre  24796  evth  24912  evthicc2  25415  ovolfsf  25426  ovolf  25437  vitalilem2  25564  vitalilem5  25567  0plef  25627  mbfi1fseqlem4  25673  xrge0f  25686  itg2addlem  25713  dvfre  25909  dvne0  25970  mdegxrf  26027  mtest  26367  psercn  26390  recosf1o  26498  logcn  26610  amgm  26955  emcllem7  26966  dchrfi  27220  dchr1re  27228  dchrisum0re  27478  padicabvf  27596  addsf  27952  negsf  28021  noseqind  28253  vtxdgfisf  29499  hlimf  31261  pjrni  31726  pjmf1  31740  2ndresdju  32676  nsgmgc  33442  mplvrpmrhm  33661  reprinfz1  34728  reprdifc  34733  bnj149  34980  subfacp1lem3  35325  mrsubrn  35656  msrf  35685  mclsind  35713  neibastop2lem  36503  weiunlem2  36606  rrncmslem  37972  cdlemk56  41170  sticksstones22  42361  hbtlem7  43309  dgraaf  43331  deg1mhm  43384  elixpconstg  45275  elmapsnd  45390  unirnmap  45394  resincncf  46061  dvnprodlem1  46132  volioof  46173  voliooicof  46182  qndenserrnbllem  46480  subsaliuncllem  46543  fge0iccico  46556  elhoi  46728  ovnsubaddlem1  46756  hoiqssbllem3  46810  ovolval4lem1  46835  rrx2xpref1o  48906  oppff1  49335  fucofulem2  49498