Theorem ffnfv 6884

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 6516	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6851	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3184	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 514	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 485	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6728	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 231	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3221	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3207	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2902	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 251	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3319	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 510	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3975	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6361	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 585	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 211	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3140  ∃wrex 3141   ⊆ wss 3938  ran crn 5558   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365

This theorem is referenced by:  ffnfvf  6885  fnfvrnss  6886  frnssb  6887  fmpt2d  6889  fconstfv  6977  ffnov  7280  seqomlem2  8089  elixpconst  8471  elixpsn  8503  unblem4  8775  ordtypelem4  8987  oismo  9006  cantnfvalf  9130  rankf  9225  alephon  9497  alephf1  9513  alephf1ALT  9531  alephfplem4  9535  cfsmolem  9694  infpssrlem3  9729  axcc4  9863  domtriomlem  9866  axdclem2  9944  pwfseqlem3  10084  gch3  10100  inar1  10199  peano5nni  11643  cnref1o  12387  seqf2  13392  hashkf  13695  iswrdsymb  13883  ccatrn  13945  shftf  14440  sqrtf  14725  isercoll2  15027  eff2  15454  reeff1  15475  1arith  16265  ramcl  16367  xpscf  16840  dmaf  17311  cdaf  17312  coapm  17333  odf  18667  gsumpt  19084  dprdff  19136  dprdfcntz  19139  dprdfadd  19144  dprdlub  19150  mgpf  19311  prdscrngd  19365  isabvd  19593  psrbagcon  20153  subrgmvrf  20245  mplbas2  20253  mvrf2  20274  psgnghm  20726  frlmsslsp  20942  kqf  22357  fmf  22555  tmdgsum2  22706  prdstmdd  22734  prdstgpd  22735  prdsxmslem2  23141  metdsre  23463  evth  23565  evthicc2  24063  ovolfsf  24074  ovolf  24085  vitalilem2  24212  vitalilem5  24215  0plef  24275  mbfi1fseqlem4  24321  xrge0f  24334  itg2addlem  24361  dvfre  24550  dvne0  24610  mdegxrf  24664  mtest  24994  psercn  25016  recosf1o  25121  logcn  25232  amgm  25570  emcllem7  25581  dchrfi  25833  dchr1re  25841  dchrisum0re  26091  padicabvf  26209  vtxdgfisf  27260  hlimf  29016  pjrni  29481  pjmf1  29495  reprinfz1  31895  reprdifc  31900  bnj149  32149  subfacp1lem3  32431  mrsubrn  32762  msrf  32791  mclsind  32819  neibastop2lem  33710  rrncmslem  35112  cdlemk56  38109  hbtlem7  39732  dgraaf  39754  deg1mhm  39814  elixpconstg  41362  elmapsnd  41474  unirnmap  41478  resincncf  42165  dvnprodlem1  42238  volioof  42279  voliooicof  42288  qndenserrnbllem  42586  subsaliuncllem  42647  fge0iccico  42659  elhoi  42831  ovnsubaddlem1  42859  hoiqssbllem3  42913  ovolval4lem1  42938  rrx2xpref1o  44712