Theorem ffnfv 6295

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 5958	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6265	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 2949	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 553	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 472	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6153	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 218	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 2925	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 2913	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2676	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 238	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 34	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3008	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 687	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3574	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 5808	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 695	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 198	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ran crn 5039   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  ffnfvf  6296  fnfvrnss  6297  frnssb  6298  fmpt2d  6300  fconstfv  6381  ffnov  6662  seqomlem2  7433  elixpconst  7802  elixpsn  7833  unblem4  8100  ordtypelem4  8309  oismo  8328  cantnfvalf  8445  rankf  8540  alephon  8775  alephf1  8791  alephf1ALT  8809  alephfplem4  8813  cfsmolem  8975  infpssrlem3  9010  axcc4  9144  domtriomlem  9147  axdclem2  9225  pwfseqlem3  9361  gch3  9377  inar1  9476  peano5nni  10900  cnref1o  11703  seqf2  12682  hashkf  12981  iswrdsymb  13177  ccatrn  13225  shftf  13667  sqrtf  13951  isercoll2  14247  eff2  14668  reeff1  14689  1arith  15469  ramcl  15571  xpscf  16049  dmaf  16522  cdaf  16523  coapm  16544  odf  17779  gsumpt  18184  dprdff  18234  dprdfcntz  18237  dprdfadd  18242  dprdlub  18248  mgpf  18382  prdscrngd  18436  isabvd  18643  psrbagcon  19192  subrgmvrf  19283  mplbas2  19291  mvrf2  19313  psgnghm  19745  frlmsslsp  19954  kqf  21360  fmf  21559  tmdgsum2  21710  prdstmdd  21737  prdstgpd  21738  prdsxmslem2  22144  metdsre  22464  evth  22566  evthicc2  23036  ovolfsf  23047  ovolf  23057  vitalilem2  23184  vitalilem5  23187  0plef  23245  mbfi1fseqlem4  23291  xrge0f  23304  itg2addlem  23331  dvfre  23520  dvne0  23578  mdegxrf  23632  mtest  23962  psercn  23984  recosf1o  24085  logcn  24193  amgm  24517  emcllem7  24528  dchrfi  24780  dchr1re  24788  dchrisum0re  25002  padicabvf  25120  hlimf  27478  pjrni  27945  pjmf1  27959  bnj149  30199  subfacp1lem3  30418  mrsubrn  30664  msrf  30693  mclsind  30721  neibastop2lem  31525  rrncmslem  32801  cdlemk56  35277  hbtlem7  36714  dgraaf  36736  deg1mhm  36804  elixpconstg  38294  elmapsnd  38391  unirnmap  38395  resincncf  38760  dvnprodlem1  38836  volioof  38880  voliooicof  38889  qndenserrnbllem  39190  subsaliuncllem  39251  fge0iccico  39263  elhoi  39432  ovnsubaddlem1  39460  hoiqssbllem3  39514  ovolval4lem1  39539  vtxdgfisf  40691  1wlkres  40879