Theorem ffnfv 7130

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 6720	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7092	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3158	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 521	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 488	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6956	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3290	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1948	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3254	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2852	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3273	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 517	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3919	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6551	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 595	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 212	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900  ran crn 5656   Fn wfn 6542  ⟶wf 6543  ‘cfv 6547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555

This theorem is used by:  ffnfvf  7131  fnfvrnss  7132  fcdmssb  7133  fmpt2d  7136  fssrescdmd  7138  fconstfv  7228  ffnov  7556  seqomlem2  8475  naddf  8705  elixpconst  8947  elixpsn  8979  unblem4  9301  ordtypelem4  9528  oismo  9547  cantnfvalf  9679  rankf  9815  alephon  10161  alephf1  10177  alephf1ALT  10195  alephfplem4  10199  cfsmolem  10361  infpssrlem3  10396  axcc4  10530  domtriomlem  10533  pwfseqlem3  10758  gch3  10774  inar1  10873  peano5nni  12351  cnref1o  13126  seqf2  14177  hashkf  14489  iswrdsymb  14689  ccatrn  14748  shftf  15247  sqrtf  15546  isercoll2  15851  eff2  16282  reeff1  16303  1arith  17120  ramcl  17222  xpscf  17752  dmaf  18239  cdaf  18240  coapm  18261  odf  19766  gsumpt  20191  dprdff  20243  dprdfcntz  20246  dprdfadd  20251  dprdlub  20257  rngmgpf  20394  mgpf  20490  prdscrngd  20566  isabvd  21084  psgnghm  21901  frlmsslsp  22117  psrbagcon  22248  mvrf2  22315  subrgmvrf  22358  mplbas2  22366  kqf  24081  fmf  24279  tmdgsum2  24430  prdstmdd  24458  prdstgpd  24459  prdsxmslem2  24863  metdsre  25188  evth  25295  evthicc2  25796  ovolfsf  25807  ovolf  25818  vitalilem2  25945  vitalilem5  25948  0plef  26008  mbfi1fseqlem4  26054  xrge0f  26067  itg2addlem  26094  dvfre  26286  dvne0  26346  mdegxrf  26401  mtest  26746  psercn  26768  recosf1o  26878  logcn  26990  amgm  27333  emcllem7  27344  dchrfi  27597  dchr1re  27605  dchrisum0re  27855  padicabvf  27973  addsf  28383  negsf  28453  noseqind  28693  vtxdgfisf  30072  hlimf  31854  pjrni  32319  pjmf1  32333  2ndresdju  33300  nsgmgc  34019  selvply1rhmlemb  34207  mplvrpmrhm  34235  reprinfz1  35307  reprdifc  35312  bnj149  35561  subfacp1lem3  36071  mrsubrn  36402  msrf  36431  mclsind  36459  neibastop2lem  37278  weiunlem  37381  mh-inf3f1  37459  rrncmslem  38909  cdlemk56  42171  sticksstones22  43361  hbtlem7  44270  dgraaf  44292  deg1mhm  44345  elixpconstg  46246  elmapsnd  46360  unirnmap  46363  resincncf  47027  dvnprodlem1  47098  volioof  47139  voliooicof  47148  qndenserrnbllem  47446  subsaliuncllem  47509  fge0iccico  47522  elhoi  47694  ovnsubaddlem1  47722  hoiqssbllem3  47776  ovolval4lem1  47801  oppff1  50406  fucofulem2  50575