Theorem ffnfv 6388

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 6045	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6357	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 2966	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 554	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 473	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6243	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 219	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 2941	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1843	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 2929	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2689	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 239	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3026	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 689	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3609	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 5892	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 698	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 199	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913   ⊆ wss 3574  ran crn 5115   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  ffnfvf  6389  fnfvrnss  6390  frnssb  6391  fmpt2d  6393  fconstfv  6476  ffnov  6764  seqomlem2  7546  elixpconst  7916  elixpsn  7947  unblem4  8215  ordtypelem4  8426  oismo  8445  cantnfvalf  8562  rankf  8657  alephon  8892  alephf1  8908  alephf1ALT  8926  alephfplem4  8930  cfsmolem  9092  infpssrlem3  9127  axcc4  9261  domtriomlem  9264  axdclem2  9342  pwfseqlem3  9482  gch3  9498  inar1  9597  peano5nni  11023  cnref1o  11827  seqf2  12820  hashkf  13119  iswrdsymb  13322  ccatrn  13372  shftf  13819  sqrtf  14103  isercoll2  14399  eff2  14829  reeff1  14850  1arith  15631  ramcl  15733  xpscf  16226  dmaf  16699  cdaf  16700  coapm  16721  odf  17956  gsumpt  18361  dprdff  18411  dprdfcntz  18414  dprdfadd  18419  dprdlub  18425  mgpf  18559  prdscrngd  18613  isabvd  18820  psrbagcon  19371  subrgmvrf  19462  mplbas2  19470  mvrf2  19492  psgnghm  19926  frlmsslsp  20135  kqf  21550  fmf  21749  tmdgsum2  21900  prdstmdd  21927  prdstgpd  21928  prdsxmslem2  22334  metdsre  22656  evth  22758  evthicc2  23229  ovolfsf  23240  ovolf  23250  vitalilem2  23378  vitalilem5  23381  0plef  23439  mbfi1fseqlem4  23485  xrge0f  23498  itg2addlem  23525  dvfre  23714  dvne0  23774  mdegxrf  23828  mtest  24158  psercn  24180  recosf1o  24281  logcn  24393  amgm  24717  emcllem7  24728  dchrfi  24980  dchr1re  24988  dchrisum0re  25202  padicabvf  25320  vtxdgfisf  26372  wlkres  26567  hlimf  28094  pjrni  28561  pjmf1  28575  reprinfz1  30700  reprdifc  30705  bnj149  30945  subfacp1lem3  31164  mrsubrn  31410  msrf  31439  mclsind  31467  neibastop2lem  32355  rrncmslem  33631  cdlemk56  36259  hbtlem7  37695  dgraaf  37717  deg1mhm  37785  elixpconstg  39266  elmapsnd  39396  unirnmap  39400  resincncf  40088  dvnprodlem1  40161  volioof  40204  voliooicof  40213  qndenserrnbllem  40514  subsaliuncllem  40575  fge0iccico  40587  elhoi  40756  ovnsubaddlem1  40784  hoiqssbllem3  40838  ovolval4lem1  40863