Theorem ffnfv 7091

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 6688	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7053	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3125	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6921	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3261	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3225	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2816	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3244	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3952	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6515	. . 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 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  ffnfvf  7092  fnfvrnss  7093  fcdmssb  7094  fmpt2d  7096  fssrescdmd  7098  fconstfv  7186  ffnov  7515  seqomlem2  8419  naddf  8645  elixpconst  8878  elixpsn  8910  unblem4  9242  ordtypelem4  9474  oismo  9493  cantnfvalf  9618  rankf  9747  alephon  10022  alephf1  10038  alephf1ALT  10056  alephfplem4  10060  cfsmolem  10223  infpssrlem3  10258  axcc4  10392  domtriomlem  10395  pwfseqlem3  10613  gch3  10629  inar1  10728  peano5nni  12189  cnref1o  12944  seqf2  13986  hashkf  14297  iswrdsymb  14496  ccatrn  14554  shftf  15045  sqrtf  15330  isercoll2  15635  eff2  16067  reeff1  16088  1arith  16898  ramcl  17000  xpscf  17528  dmaf  18011  cdaf  18012  coapm  18033  odf  19467  gsumpt  19892  dprdff  19944  dprdfcntz  19947  dprdfadd  19952  dprdlub  19958  rngmgpf  20066  mgpf  20157  prdscrngd  20231  isabvd  20721  psgnghm  21489  frlmsslsp  21705  psrbagcon  21834  mvrf2  21902  subrgmvrf  21941  mplbas2  21949  kqf  23634  fmf  23832  tmdgsum2  23983  prdstmdd  24011  prdstgpd  24012  prdsxmslem2  24417  metdsre  24742  evth  24858  evthicc2  25361  ovolfsf  25372  ovolf  25383  vitalilem2  25510  vitalilem5  25513  0plef  25573  mbfi1fseqlem4  25619  xrge0f  25632  itg2addlem  25659  dvfre  25855  dvne0  25916  mdegxrf  25973  mtest  26313  psercn  26336  recosf1o  26444  logcn  26556  amgm  26901  emcllem7  26912  dchrfi  27166  dchr1re  27174  dchrisum0re  27424  padicabvf  27542  addsf  27889  negsf  27958  noseqind  28186  vtxdgfisf  29404  hlimf  31166  pjrni  31631  pjmf1  31645  2ndresdju  32573  nsgmgc  33383  reprinfz1  34613  reprdifc  34618  bnj149  34865  subfacp1lem3  35169  mrsubrn  35500  msrf  35529  mclsind  35557  neibastop2lem  36348  weiunlem2  36451  rrncmslem  37826  cdlemk56  40965  sticksstones22  42156  hbtlem7  43114  dgraaf  43136  deg1mhm  43189  elixpconstg  45083  elmapsnd  45198  unirnmap  45202  resincncf  45873  dvnprodlem1  45944  volioof  45985  voliooicof  45994  qndenserrnbllem  46292  subsaliuncllem  46355  fge0iccico  46368  elhoi  46540  ovnsubaddlem1  46568  hoiqssbllem3  46622  ovolval4lem1  46647  rrx2xpref1o  48707  oppff1  49137  fucofulem2  49300