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 3125	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6903	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3259	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3223	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2816	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3242	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3949	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6503	. . 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 3911  ran crn 5632   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507

This theorem is referenced by:  ffnfvf  7074  fnfvrnss  7075  fcdmssb  7076  fmpt2d  7078  fssrescdmd  7080  fconstfv  7168  ffnov  7495  seqomlem2  8396  naddf  8622  elixpconst  8855  elixpsn  8887  unblem4  9218  ordtypelem4  9450  oismo  9469  cantnfvalf  9594  rankf  9723  alephon  9998  alephf1  10014  alephf1ALT  10032  alephfplem4  10036  cfsmolem  10199  infpssrlem3  10234  axcc4  10368  domtriomlem  10371  pwfseqlem3  10589  gch3  10605  inar1  10704  peano5nni  12165  cnref1o  12920  seqf2  13962  hashkf  14273  iswrdsymb  14472  ccatrn  14530  shftf  15021  sqrtf  15306  isercoll2  15611  eff2  16043  reeff1  16064  1arith  16874  ramcl  16976  xpscf  17504  dmaf  17991  cdaf  17992  coapm  18013  odf  19451  gsumpt  19876  dprdff  19928  dprdfcntz  19931  dprdfadd  19936  dprdlub  19942  rngmgpf  20077  mgpf  20168  prdscrngd  20242  isabvd  20732  psgnghm  21522  frlmsslsp  21738  psrbagcon  21867  mvrf2  21935  subrgmvrf  21974  mplbas2  21982  kqf  23667  fmf  23865  tmdgsum2  24016  prdstmdd  24044  prdstgpd  24045  prdsxmslem2  24450  metdsre  24775  evth  24891  evthicc2  25394  ovolfsf  25405  ovolf  25416  vitalilem2  25543  vitalilem5  25546  0plef  25606  mbfi1fseqlem4  25652  xrge0f  25665  itg2addlem  25692  dvfre  25888  dvne0  25949  mdegxrf  26006  mtest  26346  psercn  26369  recosf1o  26477  logcn  26589  amgm  26934  emcllem7  26945  dchrfi  27199  dchr1re  27207  dchrisum0re  27457  padicabvf  27575  addsf  27929  negsf  27998  noseqind  28226  vtxdgfisf  29457  hlimf  31216  pjrni  31681  pjmf1  31695  2ndresdju  32623  nsgmgc  33376  reprinfz1  34606  reprdifc  34611  bnj149  34858  subfacp1lem3  35162  mrsubrn  35493  msrf  35522  mclsind  35550  neibastop2lem  36341  weiunlem2  36444  rrncmslem  37819  cdlemk56  40958  sticksstones22  42149  hbtlem7  43107  dgraaf  43129  deg1mhm  43182  elixpconstg  45076  elmapsnd  45191  unirnmap  45195  resincncf  45866  dvnprodlem1  45937  volioof  45978  voliooicof  45987  qndenserrnbllem  46285  subsaliuncllem  46348  fge0iccico  46361  elhoi  46533  ovnsubaddlem1  46561  hoiqssbllem3  46615  ovolval4lem1  46640  rrx2xpref1o  48700  oppff1  49130  fucofulem2  49293