Theorem ffnfv 7138

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 6735	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7100	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3145	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6968	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3283	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1913	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3246	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2828	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3265	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3988	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6564	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 583	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 209	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069   ⊆ wss 3950  ran crn 5685   Fn wfn 6555  ⟶wf 6556  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568

This theorem is referenced by:  ffnfvf  7139  fnfvrnss  7140  fcdmssb  7141  fmpt2d  7143  fssrescdmd  7145  fconstfv  7233  ffnov  7560  seqomlem2  8492  naddf  8720  elixpconst  8946  elixpsn  8978  unblem4  9332  ordtypelem4  9562  oismo  9581  cantnfvalf  9706  rankf  9835  alephon  10110  alephf1  10126  alephf1ALT  10144  alephfplem4  10148  cfsmolem  10311  infpssrlem3  10346  axcc4  10480  domtriomlem  10483  pwfseqlem3  10701  gch3  10717  inar1  10816  peano5nni  12270  cnref1o  13028  seqf2  14063  hashkf  14372  iswrdsymb  14570  ccatrn  14628  shftf  15119  sqrtf  15403  isercoll2  15706  eff2  16136  reeff1  16157  1arith  16966  ramcl  17068  xpscf  17611  dmaf  18095  cdaf  18096  coapm  18117  odf  19556  gsumpt  19981  dprdff  20033  dprdfcntz  20036  dprdfadd  20041  dprdlub  20047  rngmgpf  20155  mgpf  20246  prdscrngd  20320  isabvd  20814  psgnghm  21599  frlmsslsp  21817  psrbagcon  21946  mvrf2  22014  subrgmvrf  22053  mplbas2  22061  kqf  23756  fmf  23954  tmdgsum2  24105  prdstmdd  24133  prdstgpd  24134  prdsxmslem2  24543  metdsre  24876  evth  24992  evthicc2  25496  ovolfsf  25507  ovolf  25518  vitalilem2  25645  vitalilem5  25648  0plef  25708  mbfi1fseqlem4  25754  xrge0f  25767  itg2addlem  25794  dvfre  25990  dvne0  26051  mdegxrf  26108  mtest  26448  psercn  26471  recosf1o  26578  logcn  26690  amgm  27035  emcllem7  27046  dchrfi  27300  dchr1re  27308  dchrisum0re  27558  padicabvf  27676  addsf  28016  negsf  28085  noseqind  28299  vtxdgfisf  29495  hlimf  31257  pjrni  31722  pjmf1  31736  2ndresdju  32660  nsgmgc  33441  reprinfz1  34638  reprdifc  34643  bnj149  34890  subfacp1lem3  35188  mrsubrn  35519  msrf  35548  mclsind  35576  neibastop2lem  36362  weiunlem2  36465  rrncmslem  37840  cdlemk56  40974  sticksstones22  42170  hbtlem7  43142  dgraaf  43164  deg1mhm  43217  elixpconstg  45099  elmapsnd  45214  unirnmap  45218  resincncf  45895  dvnprodlem1  45966  volioof  46007  voliooicof  46016  qndenserrnbllem  46314  subsaliuncllem  46377  fge0iccico  46390  elhoi  46562  ovnsubaddlem1  46590  hoiqssbllem3  46644  ovolval4lem1  46669  rrx2xpref1o  48644  fucofulem2  49029