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 6656	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7023	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3131	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 516	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 483	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6888	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 230	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3263	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1921	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3227	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2827	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 250	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3246	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 512	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3921	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6490	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 589	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 210	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063   ⊆ wss 3883  ran crn 5620   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494

This theorem is referenced by:  ffnfvf  7062  fnfvrnss  7063  fcdmssb  7064  fmpt2d  7067  fssrescdmd  7069  fconstfv  7157  ffnov  7483  seqomlem2  8381  naddf  8608  elixpconst  8844  elixpsn  8876  unblem4  9196  ordtypelem4  9427  oismo  9446  cantnfvalf  9578  rankf  9710  alephon  9983  alephf1  9999  alephf1ALT  10017  alephfplem4  10021  cfsmolem  10184  infpssrlem3  10219  axcc4  10353  domtriomlem  10356  pwfseqlem3  10575  gch3  10591  inar1  10690  peano5nni  12169  cnref1o  12927  seqf2  13975  hashkf  14286  iswrdsymb  14485  ccatrn  14544  shftf  15033  sqrtf  15318  isercoll2  15623  eff2  16058  reeff1  16079  1arith  16890  ramcl  16992  xpscf  17521  dmaf  18008  cdaf  18009  coapm  18030  odf  19504  gsumpt  19929  dprdff  19981  dprdfcntz  19984  dprdfadd  19989  dprdlub  19995  rngmgpf  20130  mgpf  20221  prdscrngd  20293  isabvd  20785  psgnghm  21556  frlmsslsp  21772  psrbagcon  21901  mvrf2  21968  subrgmvrf  22011  mplbas2  22019  kqf  23731  fmf  23929  tmdgsum2  24080  prdstmdd  24108  prdstgpd  24109  prdsxmslem2  24513  metdsre  24838  evth  24945  evthicc2  25446  ovolfsf  25457  ovolf  25468  vitalilem2  25595  vitalilem5  25598  0plef  25658  mbfi1fseqlem4  25704  xrge0f  25717  itg2addlem  25744  dvfre  25937  dvne0  25997  mdegxrf  26052  mtest  26388  psercn  26410  recosf1o  26518  logcn  26630  amgm  26973  emcllem7  26984  dchrfi  27237  dchr1re  27245  dchrisum0re  27495  padicabvf  27613  addsf  27993  negsf  28063  noseqind  28303  vtxdgfisf  29564  hlimf  31327  pjrni  31792  pjmf1  31806  2ndresdju  32742  nsgmgc  33496  selvply1rhmlemb  33712  mplvrpmrhm  33740  reprinfz1  34815  reprdifc  34820  bnj149  35066  subfacp1lem3  35419  mrsubrn  35750  msrf  35779  mclsind  35807  neibastop2lem  36597  weiunlem  36700  mh-inf3f1  36778  rrncmslem  38208  cdlemk56  41472  sticksstones22  42662  hbtlem7  43579  dgraaf  43601  deg1mhm  43654  elixpconstg  45544  elmapsnd  45658  unirnmap  45661  resincncf  46326  dvnprodlem1  46397  volioof  46438  voliooicof  46447  qndenserrnbllem  46745  subsaliuncllem  46808  fge0iccico  46821  elhoi  46993  ovnsubaddlem1  47021  hoiqssbllem3  47075  ovolval4lem1  47100  rrx2xpref1o  49217  oppff1  49646  fucofulem2  49809