Theorem ffnfv 6637

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 6278	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6606	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3175	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 509	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 476	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6490	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 221	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3150	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 2015	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3138	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2894	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 241	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3235	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 505	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3833	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6127	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 580	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 201	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166  ∀wral 3117  ∃wrex 3118   ⊆ wss 3798  ran crn 5343   Fn wfn 6118  ⟶wf 6119  ‘cfv 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131

This theorem is referenced by:  ffnfvf  6638  fnfvrnss  6639  frnssb  6640  fmpt2d  6642  fconstfv  6732  ffnov  7024  seqomlem2  7812  elixpconst  8183  elixpsn  8214  unblem4  8484  ordtypelem4  8695  oismo  8714  cantnfvalf  8839  rankf  8934  alephon  9205  alephf1  9221  alephf1ALT  9239  alephfplem4  9243  cfsmolem  9407  infpssrlem3  9442  axcc4  9576  domtriomlem  9579  axdclem2  9657  pwfseqlem3  9797  gch3  9813  inar1  9912  peano5nni  11353  cnref1o  12107  seqf2  13114  hashkf  13412  iswrdsymb  13591  ccatrn  13649  shftf  14196  sqrtf  14480  isercoll2  14776  eff2  15201  reeff1  15222  1arith  16002  ramcl  16104  xpscf  16579  dmaf  17051  cdaf  17052  coapm  17073  odf  18307  gsumpt  18714  dprdff  18765  dprdfcntz  18768  dprdfadd  18773  dprdlub  18779  mgpf  18913  prdscrngd  18967  isabvd  19176  psrbagcon  19732  subrgmvrf  19823  mplbas2  19831  mvrf2  19852  psgnghm  20285  frlmsslsp  20502  kqf  21921  fmf  22119  tmdgsum2  22270  prdstmdd  22297  prdstgpd  22298  prdsxmslem2  22704  metdsre  23026  evth  23128  evthicc2  23626  ovolfsf  23637  ovolf  23648  vitalilem2  23775  vitalilem5  23778  0plef  23838  mbfi1fseqlem4  23884  xrge0f  23897  itg2addlem  23924  dvfre  24113  dvne0  24173  mdegxrf  24227  mtest  24557  psercn  24579  recosf1o  24681  logcn  24792  amgm  25130  emcllem7  25141  dchrfi  25393  dchr1re  25401  dchrisum0re  25615  padicabvf  25733  vtxdgfisf  26774  wlkresOLD  26971  hlimf  28649  pjrni  29116  pjmf1  29130  reprinfz1  31249  reprdifc  31254  bnj149  31491  subfacp1lem3  31710  mrsubrn  31956  msrf  31985  mclsind  32013  neibastop2lem  32893  rrncmslem  34173  cdlemk56  37046  hbtlem7  38538  dgraaf  38560  deg1mhm  38628  elixpconstg  40083  elmapsnd  40202  unirnmap  40206  resincncf  40883  dvnprodlem1  40956  volioof  40998  voliooicof  41007  qndenserrnbllem  41305  subsaliuncllem  41366  fge0iccico  41378  elhoi  41550  ovnsubaddlem1  41578  hoiqssbllem3  41632  ovolval4lem1  41657