Theorem ffnfv 6992

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 6600	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6959	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3103	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 512	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 483	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6830	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 228	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3144	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3131	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2826	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 248	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3250	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 508	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3927	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6437	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 583	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 208	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065   ⊆ wss 3887  ran crn 5590   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441

This theorem is referenced by:  ffnfvf  6993  fnfvrnss  6994  frnssb  6995  fmpt2d  6997  fconstfv  7088  ffnov  7401  seqomlem2  8282  elixpconst  8693  elixpsn  8725  unblem4  9069  ordtypelem4  9280  oismo  9299  cantnfvalf  9423  rankf  9552  alephon  9825  alephf1  9841  alephf1ALT  9859  alephfplem4  9863  cfsmolem  10026  infpssrlem3  10061  axcc4  10195  domtriomlem  10198  pwfseqlem3  10416  gch3  10432  inar1  10531  peano5nni  11976  cnref1o  12725  seqf2  13742  hashkf  14046  iswrdsymb  14234  ccatrn  14294  shftf  14790  sqrtf  15075  isercoll2  15380  eff2  15808  reeff1  15829  1arith  16628  ramcl  16730  xpscf  17276  dmaf  17764  cdaf  17765  coapm  17786  odf  19145  gsumpt  19563  dprdff  19615  dprdfcntz  19618  dprdfadd  19623  dprdlub  19629  mgpf  19798  prdscrngd  19852  isabvd  20080  psgnghm  20785  frlmsslsp  21003  psrbagcon  21133  psrbagconOLD  21134  subrgmvrf  21235  mplbas2  21243  mvrf2  21268  kqf  22898  fmf  23096  tmdgsum2  23247  prdstmdd  23275  prdstgpd  23276  prdsxmslem2  23685  metdsre  24016  evth  24122  evthicc2  24624  ovolfsf  24635  ovolf  24646  vitalilem2  24773  vitalilem5  24776  0plef  24836  mbfi1fseqlem4  24883  xrge0f  24896  itg2addlem  24923  dvfre  25115  dvne0  25175  mdegxrf  25233  mtest  25563  psercn  25585  recosf1o  25691  logcn  25802  amgm  26140  emcllem7  26151  dchrfi  26403  dchr1re  26411  dchrisum0re  26661  padicabvf  26779  vtxdgfisf  27843  hlimf  29599  pjrni  30064  pjmf1  30078  2ndresdju  30986  nsgmgc  31597  reprinfz1  32602  reprdifc  32607  bnj149  32855  subfacp1lem3  33144  mrsubrn  33475  msrf  33504  mclsind  33532  neibastop2lem  34549  rrncmslem  35990  cdlemk56  38985  sticksstones22  40124  hbtlem7  40950  dgraaf  40972  deg1mhm  41032  elixpconstg  42639  elmapsnd  42744  unirnmap  42748  resincncf  43416  dvnprodlem1  43487  volioof  43528  voliooicof  43537  qndenserrnbllem  43835  subsaliuncllem  43896  fge0iccico  43908  elhoi  44080  ovnsubaddlem1  44108  hoiqssbllem3  44162  ovolval4lem1  44187  rrx2xpref1o  46064