Theorem ffnfv 7042

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 6645	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7009	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3139	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 512	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 483	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6880	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 228	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3263	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3226	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2824	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 248	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3245	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 508	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3937	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6477	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 583	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 208	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∀wral 3061  ∃wrex 3070   ⊆ wss 3897  ran crn 5615   Fn wfn 6468  ⟶wf 6469  ‘cfv 6473

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-fv 6481

This theorem is referenced by:  ffnfvf  7043  fnfvrnss  7044  fcdmssb  7045  fmpt2d  7047  fconstfv  7138  ffnov  7455  seqomlem2  8344  elixpconst  8756  elixpsn  8788  unblem4  9155  ordtypelem4  9370  oismo  9389  cantnfvalf  9514  rankf  9643  alephon  9918  alephf1  9934  alephf1ALT  9952  alephfplem4  9956  cfsmolem  10119  infpssrlem3  10154  axcc4  10288  domtriomlem  10291  pwfseqlem3  10509  gch3  10525  inar1  10624  peano5nni  12069  cnref1o  12818  seqf2  13835  hashkf  14139  iswrdsymb  14326  ccatrn  14385  shftf  14881  sqrtf  15166  isercoll2  15471  eff2  15899  reeff1  15920  1arith  16717  ramcl  16819  xpscf  17365  dmaf  17853  cdaf  17854  coapm  17875  odf  19233  gsumpt  19650  dprdff  19702  dprdfcntz  19705  dprdfadd  19710  dprdlub  19716  mgpf  19885  prdscrngd  19939  isabvd  20178  psgnghm  20883  frlmsslsp  21101  psrbagcon  21231  psrbagconOLD  21232  subrgmvrf  21333  mplbas2  21341  mvrf2  21366  kqf  22996  fmf  23194  tmdgsum2  23345  prdstmdd  23373  prdstgpd  23374  prdsxmslem2  23783  metdsre  24114  evth  24220  evthicc2  24722  ovolfsf  24733  ovolf  24744  vitalilem2  24871  vitalilem5  24874  0plef  24934  mbfi1fseqlem4  24981  xrge0f  24994  itg2addlem  25021  dvfre  25213  dvne0  25273  mdegxrf  25331  mtest  25661  psercn  25683  recosf1o  25789  logcn  25900  amgm  26238  emcllem7  26249  dchrfi  26501  dchr1re  26509  dchrisum0re  26759  padicabvf  26877  vtxdgfisf  28073  hlimf  29828  pjrni  30293  pjmf1  30307  2ndresdju  31214  nsgmgc  31835  reprinfz1  32843  reprdifc  32848  bnj149  33095  subfacp1lem3  33384  mrsubrn  33715  msrf  33744  mclsind  33772  neibastop2lem  34640  rrncmslem  36088  cdlemk56  39232  sticksstones22  40374  hbtlem7  41201  dgraaf  41223  deg1mhm  41283  elixpconstg  42948  elmapsnd  43060  unirnmap  43064  resincncf  43741  dvnprodlem1  43812  volioof  43853  voliooicof  43862  qndenserrnbllem  44160  subsaliuncllem  44221  fge0iccico  44234  elhoi  44406  ovnsubaddlem1  44434  hoiqssbllem3  44488  ovolval4lem1  44513  rrx2xpref1o  46404