Theorem ffnfv 7114

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 6711	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7076	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3133	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6944	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3270	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3234	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2823	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3253	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3969	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6540	. . 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 3052  ∃wrex 3061   ⊆ wss 3931  ran crn 5660   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  ffnfvf  7115  fnfvrnss  7116  fcdmssb  7117  fmpt2d  7119  fssrescdmd  7121  fconstfv  7209  ffnov  7538  seqomlem2  8470  naddf  8698  elixpconst  8924  elixpsn  8956  unblem4  9308  ordtypelem4  9540  oismo  9559  cantnfvalf  9684  rankf  9813  alephon  10088  alephf1  10104  alephf1ALT  10122  alephfplem4  10126  cfsmolem  10289  infpssrlem3  10324  axcc4  10458  domtriomlem  10461  pwfseqlem3  10679  gch3  10695  inar1  10794  peano5nni  12248  cnref1o  13006  seqf2  14044  hashkf  14355  iswrdsymb  14554  ccatrn  14612  shftf  15103  sqrtf  15387  isercoll2  15690  eff2  16122  reeff1  16143  1arith  16952  ramcl  17054  xpscf  17584  dmaf  18067  cdaf  18068  coapm  18089  odf  19523  gsumpt  19948  dprdff  20000  dprdfcntz  20003  dprdfadd  20008  dprdlub  20014  rngmgpf  20122  mgpf  20213  prdscrngd  20287  isabvd  20777  psgnghm  21545  frlmsslsp  21761  psrbagcon  21890  mvrf2  21958  subrgmvrf  21997  mplbas2  22005  kqf  23690  fmf  23888  tmdgsum2  24039  prdstmdd  24067  prdstgpd  24068  prdsxmslem2  24473  metdsre  24798  evth  24914  evthicc2  25418  ovolfsf  25429  ovolf  25440  vitalilem2  25567  vitalilem5  25570  0plef  25630  mbfi1fseqlem4  25676  xrge0f  25689  itg2addlem  25716  dvfre  25912  dvne0  25973  mdegxrf  26030  mtest  26370  psercn  26393  recosf1o  26501  logcn  26613  amgm  26958  emcllem7  26969  dchrfi  27223  dchr1re  27231  dchrisum0re  27481  padicabvf  27599  addsf  27946  negsf  28015  noseqind  28243  vtxdgfisf  29461  hlimf  31223  pjrni  31688  pjmf1  31702  2ndresdju  32632  nsgmgc  33432  reprinfz1  34659  reprdifc  34664  bnj149  34911  subfacp1lem3  35209  mrsubrn  35540  msrf  35569  mclsind  35597  neibastop2lem  36383  weiunlem2  36486  rrncmslem  37861  cdlemk56  40995  sticksstones22  42186  hbtlem7  43124  dgraaf  43146  deg1mhm  43199  elixpconstg  45093  elmapsnd  45208  unirnmap  45212  resincncf  45884  dvnprodlem1  45955  volioof  45996  voliooicof  46005  qndenserrnbllem  46303  subsaliuncllem  46366  fge0iccico  46379  elhoi  46551  ovnsubaddlem1  46579  hoiqssbllem3  46633  ovolval4lem1  46658  rrx2xpref1o  48678  fucofulem2  49202