Theorem ffnfv 7115

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 6706	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7077	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3163	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 520	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 487	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6942	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3295	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1941	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3259	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2857	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3278	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 516	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3951	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6541	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 594	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 212	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095   ⊆ wss 3913  ran crn 5663   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is referenced by:  ffnfvf  7116  fnfvrnss  7117  fcdmssb  7118  fmpt2d  7121  fssrescdmd  7123  fconstfv  7211  ffnov  7537  seqomlem2  8438  naddf  8668  elixpconst  8903  elixpsn  8935  unblem4  9255  ordtypelem4  9483  oismo  9502  cantnfvalf  9634  rankf  9766  alephon  10053  alephf1  10069  alephf1ALT  10087  alephfplem4  10091  cfsmolem  10254  infpssrlem3  10289  axcc4  10423  domtriomlem  10426  pwfseqlem3  10645  gch3  10661  inar1  10760  peano5nni  12236  cnref1o  13009  seqf2  14057  hashkf  14368  iswrdsymb  14568  ccatrn  14627  shftf  15116  sqrtf  15415  isercoll2  15720  eff2  16155  reeff1  16176  1arith  16987  ramcl  17089  xpscf  17619  dmaf  18106  cdaf  18107  coapm  18128  odf  19607  gsumpt  20032  dprdff  20084  dprdfcntz  20087  dprdfadd  20092  dprdlub  20098  rngmgpf  20235  mgpf  20330  prdscrngd  20403  isabvd  20893  psgnghm  21699  frlmsslsp  21915  psrbagcon  22044  mvrf2  22111  subrgmvrf  22154  mplbas2  22162  kqf  23873  fmf  24071  tmdgsum2  24222  prdstmdd  24250  prdstgpd  24251  prdsxmslem2  24655  metdsre  24980  evth  25087  evthicc2  25588  ovolfsf  25599  ovolf  25610  vitalilem2  25737  vitalilem5  25740  0plef  25800  mbfi1fseqlem4  25846  xrge0f  25859  itg2addlem  25886  dvfre  26079  dvne0  26139  mdegxrf  26194  mtest  26533  psercn  26555  recosf1o  26666  logcn  26778  amgm  27121  emcllem7  27132  dchrfi  27385  dchr1re  27393  dchrisum0re  27643  padicabvf  27761  addsf  28141  negsf  28211  noseqind  28451  vtxdgfisf  29767  hlimf  31530  pjrni  31995  pjmf1  32009  2ndresdju  32935  nsgmgc  33665  selvply1rhmlemb  33854  mplvrpmrhm  33882  reprinfz1  34954  reprdifc  34959  bnj149  35208  subfacp1lem3  35607  mrsubrn  35938  msrf  35967  mclsind  35995  neibastop2lem  36794  weiunlem  36897  mh-inf3f1  36975  rrncmslem  38405  cdlemk56  41669  sticksstones22  42859  hbtlem7  43778  dgraaf  43800  deg1mhm  43853  elixpconstg  45733  elmapsnd  45847  unirnmap  45850  resincncf  46515  dvnprodlem1  46586  volioof  46627  voliooicof  46636  qndenserrnbllem  46934  subsaliuncllem  46997  fge0iccico  47010  elhoi  47182  ovnsubaddlem1  47210  hoiqssbllem3  47264  ovolval4lem1  47289  rrx2xpref1o  49417  oppff1  49845  fucofulem2  50008