Theorem ffnfv 7073

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 6670	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7035	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3130	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6902	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3226	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2825	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3245	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3941	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6504	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 584	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 209	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  ffnfvf  7074  fnfvrnss  7075  fcdmssb  7076  fmpt2d  7079  fssrescdmd  7081  fconstfv  7168  ffnov  7494  seqomlem2  8392  naddf  8619  elixpconst  8855  elixpsn  8887  unblem4  9207  ordtypelem4  9438  oismo  9457  cantnfvalf  9586  rankf  9718  alephon  9991  alephf1  10007  alephf1ALT  10025  alephfplem4  10029  cfsmolem  10192  infpssrlem3  10227  axcc4  10361  domtriomlem  10364  pwfseqlem3  10583  gch3  10599  inar1  10698  peano5nni  12160  cnref1o  12910  seqf2  13956  hashkf  14267  iswrdsymb  14466  ccatrn  14525  shftf  15014  sqrtf  15299  isercoll2  15604  eff2  16036  reeff1  16057  1arith  16867  ramcl  16969  xpscf  17498  dmaf  17985  cdaf  17986  coapm  18007  odf  19481  gsumpt  19906  dprdff  19958  dprdfcntz  19961  dprdfadd  19966  dprdlub  19972  rngmgpf  20107  mgpf  20198  prdscrngd  20272  isabvd  20760  psgnghm  21550  frlmsslsp  21766  psrbagcon  21896  mvrf2  21963  subrgmvrf  22004  mplbas2  22012  kqf  23706  fmf  23904  tmdgsum2  24055  prdstmdd  24083  prdstgpd  24084  prdsxmslem2  24488  metdsre  24813  evth  24929  evthicc2  25432  ovolfsf  25443  ovolf  25454  vitalilem2  25581  vitalilem5  25584  0plef  25644  mbfi1fseqlem4  25690  xrge0f  25703  itg2addlem  25730  dvfre  25926  dvne0  25987  mdegxrf  26044  mtest  26384  psercn  26407  recosf1o  26515  logcn  26627  amgm  26972  emcllem7  26983  dchrfi  27237  dchr1re  27245  dchrisum0re  27495  padicabvf  27613  addsf  27993  negsf  28063  noseqind  28303  vtxdgfisf  29566  hlimf  31329  pjrni  31794  pjmf1  31808  2ndresdju  32743  nsgmgc  33509  mplvrpmrhm  33728  reprinfz1  34804  reprdifc  34809  bnj149  35055  subfacp1lem3  35402  mrsubrn  35733  msrf  35762  mclsind  35790  neibastop2lem  36580  weiunlem  36683  rrncmslem  38087  cdlemk56  41351  sticksstones22  42542  hbtlem7  43486  dgraaf  43508  deg1mhm  43561  elixpconstg  45452  elmapsnd  45566  unirnmap  45570  resincncf  46237  dvnprodlem1  46308  volioof  46349  voliooicof  46358  qndenserrnbllem  46656  subsaliuncllem  46719  fge0iccico  46732  elhoi  46904  ovnsubaddlem1  46932  hoiqssbllem3  46986  ovolval4lem1  47011  rrx2xpref1o  49082  oppff1  49511  fucofulem2  49674