Theorem ffnfv 7118

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 6709	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7080	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3159	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 521	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 488	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6945	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3291	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3255	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2853	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3274	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 517	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3944	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6544	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 595	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 212	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091   ⊆ wss 3906  ran crn 5664   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  ffnfvf  7119  fnfvrnss  7120  fcdmssb  7121  fmpt2d  7124  fssrescdmd  7126  fconstfv  7217  ffnov  7545  seqomlem2  8444  naddf  8674  elixpconst  8909  elixpsn  8941  unblem4  9262  ordtypelem4  9490  oismo  9509  cantnfvalf  9641  rankf  9773  alephon  10069  alephf1  10085  alephf1ALT  10103  alephfplem4  10107  cfsmolem  10269  infpssrlem3  10304  axcc4  10438  domtriomlem  10441  pwfseqlem3  10662  gch3  10678  inar1  10777  peano5nni  12253  cnref1o  13027  seqf2  14077  hashkf  14388  iswrdsymb  14588  ccatrn  14647  shftf  15142  sqrtf  15441  isercoll2  15746  eff2  16179  reeff1  16200  1arith  17011  ramcl  17113  xpscf  17643  dmaf  18130  cdaf  18131  coapm  18152  odf  19653  gsumpt  20078  dprdff  20130  dprdfcntz  20133  dprdfadd  20138  dprdlub  20144  rngmgpf  20281  mgpf  20376  prdscrngd  20451  isabvd  20967  psgnghm  21782  frlmsslsp  21998  psrbagcon  22127  mvrf2  22194  subrgmvrf  22237  mplbas2  22245  kqf  23957  fmf  24155  tmdgsum2  24306  prdstmdd  24334  prdstgpd  24335  prdsxmslem2  24739  metdsre  25064  evth  25171  evthicc2  25672  ovolfsf  25683  ovolf  25694  vitalilem2  25821  vitalilem5  25824  0plef  25884  mbfi1fseqlem4  25930  xrge0f  25943  itg2addlem  25970  dvfre  26163  dvne0  26223  mdegxrf  26278  mtest  26620  psercn  26642  recosf1o  26753  logcn  26865  amgm  27208  emcllem7  27219  dchrfi  27472  dchr1re  27480  dchrisum0re  27730  padicabvf  27848  addsf  28228  negsf  28298  noseqind  28538  vtxdgfisf  29886  hlimf  31662  pjrni  32127  pjmf1  32141  2ndresdju  33067  nsgmgc  33787  selvply1rhmlemb  33975  mplvrpmrhm  34003  reprinfz1  35076  reprdifc  35081  bnj149  35330  subfacp1lem3  35713  mrsubrn  36044  msrf  36073  mclsind  36101  neibastop2lem  36930  weiunlem  37033  mh-inf3f1  37111  rrncmslem  38543  cdlemk56  41805  sticksstones22  42995  hbtlem7  43912  dgraaf  43934  deg1mhm  43987  elixpconstg  45867  elmapsnd  45981  unirnmap  45984  resincncf  46649  dvnprodlem1  46720  volioof  46761  voliooicof  46770  qndenserrnbllem  47068  subsaliuncllem  47131  fge0iccico  47144  elhoi  47316  ovnsubaddlem1  47344  hoiqssbllem3  47398  ovolval4lem1  47423  rrx2xpref1o  49557  oppff1  49985  fucofulem2  50148