Theorem ffnfv 7123

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 6716	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7085	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3141	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6953	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 228	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3276	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1910	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3239	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2816	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 248	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3258	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3984	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6546	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 582	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 208	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∀wral 3056  ∃wrex 3065   ⊆ wss 3944  ran crn 5673   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  ffnfvf  7124  fnfvrnss  7125  fcdmssb  7126  fmpt2d  7128  fconstfv  7218  ffnov  7541  seqomlem2  8465  naddf  8695  elixpconst  8915  elixpsn  8947  unblem4  9314  ordtypelem4  9536  oismo  9555  cantnfvalf  9680  rankf  9809  alephon  10084  alephf1  10100  alephf1ALT  10118  alephfplem4  10122  cfsmolem  10285  infpssrlem3  10320  axcc4  10454  domtriomlem  10457  pwfseqlem3  10675  gch3  10691  inar1  10790  peano5nni  12237  cnref1o  12991  seqf2  14010  hashkf  14315  iswrdsymb  14505  ccatrn  14563  shftf  15050  sqrtf  15334  isercoll2  15639  eff2  16067  reeff1  16088  1arith  16887  ramcl  16989  xpscf  17538  dmaf  18029  cdaf  18030  coapm  18051  odf  19483  gsumpt  19908  dprdff  19960  dprdfcntz  19963  dprdfadd  19968  dprdlub  19974  rngmgpf  20088  mgpf  20179  prdscrngd  20247  isabvd  20689  psgnghm  21499  frlmsslsp  21717  psrbagcon  21850  psrbagconOLD  21851  mvrf2  21922  subrgmvrf  21959  mplbas2  21967  kqf  23638  fmf  23836  tmdgsum2  23987  prdstmdd  24015  prdstgpd  24016  prdsxmslem2  24425  metdsre  24756  evth  24872  evthicc2  25376  ovolfsf  25387  ovolf  25398  vitalilem2  25525  vitalilem5  25528  0plef  25588  mbfi1fseqlem4  25635  xrge0f  25648  itg2addlem  25675  dvfre  25870  dvne0  25931  mdegxrf  25991  mtest  26327  psercn  26350  recosf1o  26456  logcn  26568  amgm  26910  emcllem7  26921  dchrfi  27175  dchr1re  27183  dchrisum0re  27433  padicabvf  27551  addsf  27886  negsf  27951  noseqind  28152  vtxdgfisf  29277  hlimf  31034  pjrni  31499  pjmf1  31513  2ndresdju  32418  nsgmgc  33062  reprinfz1  34190  reprdifc  34195  bnj149  34442  subfacp1lem3  34728  mrsubrn  35059  msrf  35088  mclsind  35116  neibastop2lem  35780  rrncmslem  37240  cdlemk56  40381  sticksstones22  41572  hbtlem7  42471  dgraaf  42493  deg1mhm  42551  elixpconstg  44378  elmapsnd  44500  unirnmap  44504  resincncf  45186  dvnprodlem1  45257  volioof  45298  voliooicof  45307  qndenserrnbllem  45605  subsaliuncllem  45668  fge0iccico  45681  elhoi  45853  ovnsubaddlem1  45881  hoiqssbllem3  45935  ovolval4lem1  45960  rrx2xpref1o  47714