Theorem ffnfv 7053

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 6652	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7015	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3121	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6883	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3253	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3217	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2816	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3236	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3941	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6486	. . 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 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   ⊆ wss 3903  ran crn 5620   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490

This theorem is referenced by:  ffnfvf  7054  fnfvrnss  7055  fcdmssb  7056  fmpt2d  7058  fssrescdmd  7060  fconstfv  7148  ffnov  7475  seqomlem2  8373  naddf  8599  elixpconst  8832  elixpsn  8864  unblem4  9184  ordtypelem4  9413  oismo  9432  cantnfvalf  9561  rankf  9690  alephon  9963  alephf1  9979  alephf1ALT  9997  alephfplem4  10001  cfsmolem  10164  infpssrlem3  10199  axcc4  10333  domtriomlem  10336  pwfseqlem3  10554  gch3  10570  inar1  10669  peano5nni  12131  cnref1o  12886  seqf2  13928  hashkf  14239  iswrdsymb  14438  ccatrn  14496  shftf  14986  sqrtf  15271  isercoll2  15576  eff2  16008  reeff1  16029  1arith  16839  ramcl  16941  xpscf  17469  dmaf  17956  cdaf  17957  coapm  17978  odf  19416  gsumpt  19841  dprdff  19893  dprdfcntz  19896  dprdfadd  19901  dprdlub  19907  rngmgpf  20042  mgpf  20133  prdscrngd  20207  isabvd  20697  psgnghm  21487  frlmsslsp  21703  psrbagcon  21832  mvrf2  21900  subrgmvrf  21939  mplbas2  21947  kqf  23632  fmf  23830  tmdgsum2  23981  prdstmdd  24009  prdstgpd  24010  prdsxmslem2  24415  metdsre  24740  evth  24856  evthicc2  25359  ovolfsf  25370  ovolf  25381  vitalilem2  25508  vitalilem5  25511  0plef  25571  mbfi1fseqlem4  25617  xrge0f  25630  itg2addlem  25657  dvfre  25853  dvne0  25914  mdegxrf  25971  mtest  26311  psercn  26334  recosf1o  26442  logcn  26554  amgm  26899  emcllem7  26910  dchrfi  27164  dchr1re  27172  dchrisum0re  27422  padicabvf  27540  addsf  27894  negsf  27963  noseqind  28191  vtxdgfisf  29422  hlimf  31181  pjrni  31646  pjmf1  31660  2ndresdju  32593  nsgmgc  33350  reprinfz1  34596  reprdifc  34601  bnj149  34848  subfacp1lem3  35165  mrsubrn  35496  msrf  35525  mclsind  35553  neibastop2lem  36344  weiunlem2  36447  rrncmslem  37822  cdlemk56  40960  sticksstones22  42151  hbtlem7  43108  dgraaf  43130  deg1mhm  43183  elixpconstg  45077  elmapsnd  45192  unirnmap  45196  resincncf  45866  dvnprodlem1  45937  volioof  45978  voliooicof  45987  qndenserrnbllem  46285  subsaliuncllem  46348  fge0iccico  46361  elhoi  46533  ovnsubaddlem1  46561  hoiqssbllem3  46615  ovolval4lem1  46640  rrx2xpref1o  48713  oppff1  49143  fucofulem2  49306