Theorem ffnfv 6877

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 6509	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6844	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3182	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 514	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 485	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6721	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 231	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3219	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1911	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3205	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2900	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 251	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3317	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 510	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3973	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6354	. . 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 1533   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139   ⊆ wss 3936  ran crn 5551   Fn wfn 6345  ⟶wf 6346  ‘cfv 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-fv 6358

This theorem is referenced by:  ffnfvf  6878  fnfvrnss  6879  frnssb  6880  fmpt2d  6882  fconstfv  6969  ffnov  7272  seqomlem2  8081  elixpconst  8463  elixpsn  8495  unblem4  8767  ordtypelem4  8979  oismo  8998  cantnfvalf  9122  rankf  9217  alephon  9489  alephf1  9505  alephf1ALT  9523  alephfplem4  9527  cfsmolem  9686  infpssrlem3  9721  axcc4  9855  domtriomlem  9858  axdclem2  9936  pwfseqlem3  10076  gch3  10092  inar1  10191  peano5nni  11635  cnref1o  12378  seqf2  13383  hashkf  13686  iswrdsymb  13875  ccatrn  13937  shftf  14432  sqrtf  14717  isercoll2  15019  eff2  15446  reeff1  15467  1arith  16257  ramcl  16359  xpscf  16832  dmaf  17303  cdaf  17304  coapm  17325  odf  18659  gsumpt  19076  dprdff  19128  dprdfcntz  19131  dprdfadd  19136  dprdlub  19142  mgpf  19303  prdscrngd  19357  isabvd  19585  psrbagcon  20145  subrgmvrf  20237  mplbas2  20245  mvrf2  20266  psgnghm  20718  frlmsslsp  20934  kqf  22349  fmf  22547  tmdgsum2  22698  prdstmdd  22726  prdstgpd  22727  prdsxmslem2  23133  metdsre  23455  evth  23557  evthicc2  24055  ovolfsf  24066  ovolf  24077  vitalilem2  24204  vitalilem5  24207  0plef  24267  mbfi1fseqlem4  24313  xrge0f  24326  itg2addlem  24353  dvfre  24542  dvne0  24602  mdegxrf  24656  mtest  24986  psercn  25008  recosf1o  25113  logcn  25224  amgm  25562  emcllem7  25573  dchrfi  25825  dchr1re  25833  dchrisum0re  26083  padicabvf  26201  vtxdgfisf  27252  hlimf  29008  pjrni  29473  pjmf1  29487  reprinfz1  31888  reprdifc  31893  bnj149  32142  subfacp1lem3  32424  mrsubrn  32755  msrf  32784  mclsind  32812  neibastop2lem  33703  rrncmslem  35104  cdlemk56  38101  hbtlem7  39718  dgraaf  39740  deg1mhm  39800  elixpconstg  41348  elmapsnd  41459  unirnmap  41463  resincncf  42150  dvnprodlem1  42223  volioof  42265  voliooicof  42274  qndenserrnbllem  42572  subsaliuncllem  42633  fge0iccico  42645  elhoi  42817  ovnsubaddlem1  42845  hoiqssbllem3  42899  ovolval4lem1  42924  rrx2xpref1o  44698