Theorem ffnfv 7139

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 6737	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7101	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3144	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 482	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6969	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 229	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3282	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1912	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3245	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2827	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 249	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3264	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 507	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 4001	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6567	. . 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 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068   ⊆ wss 3963  ran crn 5690   Fn wfn 6558  ⟶wf 6559  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571

This theorem is referenced by:  ffnfvf  7140  fnfvrnss  7141  fcdmssb  7142  fmpt2d  7144  fssrescdmd  7146  fconstfv  7232  ffnov  7559  seqomlem2  8490  naddf  8718  elixpconst  8944  elixpsn  8976  unblem4  9329  ordtypelem4  9559  oismo  9578  cantnfvalf  9703  rankf  9832  alephon  10107  alephf1  10123  alephf1ALT  10141  alephfplem4  10145  cfsmolem  10308  infpssrlem3  10343  axcc4  10477  domtriomlem  10480  pwfseqlem3  10698  gch3  10714  inar1  10813  peano5nni  12267  cnref1o  13025  seqf2  14059  hashkf  14368  iswrdsymb  14566  ccatrn  14624  shftf  15115  sqrtf  15399  isercoll2  15702  eff2  16132  reeff1  16153  1arith  16961  ramcl  17063  xpscf  17612  dmaf  18103  cdaf  18104  coapm  18125  odf  19570  gsumpt  19995  dprdff  20047  dprdfcntz  20050  dprdfadd  20055  dprdlub  20061  rngmgpf  20175  mgpf  20266  prdscrngd  20336  isabvd  20830  psgnghm  21616  frlmsslsp  21834  psrbagcon  21963  mvrf2  22031  subrgmvrf  22070  mplbas2  22078  kqf  23771  fmf  23969  tmdgsum2  24120  prdstmdd  24148  prdstgpd  24149  prdsxmslem2  24558  metdsre  24889  evth  25005  evthicc2  25509  ovolfsf  25520  ovolf  25531  vitalilem2  25658  vitalilem5  25661  0plef  25721  mbfi1fseqlem4  25768  xrge0f  25781  itg2addlem  25808  dvfre  26004  dvne0  26065  mdegxrf  26122  mtest  26462  psercn  26485  recosf1o  26592  logcn  26704  amgm  27049  emcllem7  27060  dchrfi  27314  dchr1re  27322  dchrisum0re  27572  padicabvf  27690  addsf  28030  negsf  28099  noseqind  28313  vtxdgfisf  29509  hlimf  31266  pjrni  31731  pjmf1  31745  2ndresdju  32666  nsgmgc  33420  reprinfz1  34616  reprdifc  34621  bnj149  34868  subfacp1lem3  35167  mrsubrn  35498  msrf  35527  mclsind  35555  neibastop2lem  36343  weiunlem2  36446  rrncmslem  37819  cdlemk56  40954  sticksstones22  42150  hbtlem7  43114  dgraaf  43136  deg1mhm  43189  elixpconstg  45029  elmapsnd  45147  unirnmap  45151  resincncf  45831  dvnprodlem1  45902  volioof  45943  voliooicof  45952  qndenserrnbllem  46250  subsaliuncllem  46313  fge0iccico  46326  elhoi  46498  ovnsubaddlem1  46526  hoiqssbllem3  46580  ovolval4lem1  46605  rrx2xpref1o  48568