Theorem ffnfv 7114

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 6705	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7076	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3157	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 520	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 487	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6941	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3289	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3253	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2851	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3272	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 516	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3943	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6540	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 594	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 212	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089   ⊆ wss 3905  ran crn 5662   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  ffnfvf  7115  fnfvrnss  7116  fcdmssb  7117  fmpt2d  7120  fssrescdmd  7122  fconstfv  7210  ffnov  7536  seqomlem2  8434  naddf  8664  elixpconst  8899  elixpsn  8931  unblem4  9251  ordtypelem4  9479  oismo  9498  cantnfvalf  9630  rankf  9762  alephon  10049  alephf1  10065  alephf1ALT  10083  alephfplem4  10087  cfsmolem  10249  infpssrlem3  10284  axcc4  10418  domtriomlem  10421  pwfseqlem3  10640  gch3  10656  inar1  10755  peano5nni  12231  cnref1o  13004  seqf2  14053  hashkf  14364  iswrdsymb  14564  ccatrn  14623  shftf  15112  sqrtf  15411  isercoll2  15716  eff2  16150  reeff1  16171  1arith  16982  ramcl  17084  xpscf  17614  dmaf  18101  cdaf  18102  coapm  18123  odf  19602  gsumpt  20027  dprdff  20079  dprdfcntz  20082  dprdfadd  20087  dprdlub  20093  rngmgpf  20230  mgpf  20325  prdscrngd  20399  isabvd  20915  psgnghm  21730  frlmsslsp  21946  psrbagcon  22075  mvrf2  22142  subrgmvrf  22185  mplbas2  22193  kqf  23904  fmf  24102  tmdgsum2  24253  prdstmdd  24281  prdstgpd  24282  prdsxmslem2  24686  metdsre  25011  evth  25118  evthicc2  25619  ovolfsf  25630  ovolf  25641  vitalilem2  25768  vitalilem5  25771  0plef  25831  mbfi1fseqlem4  25877  xrge0f  25890  itg2addlem  25917  dvfre  26110  dvne0  26170  mdegxrf  26225  mtest  26567  psercn  26589  recosf1o  26700  logcn  26812  amgm  27155  emcllem7  27166  dchrfi  27419  dchr1re  27427  dchrisum0re  27677  padicabvf  27795  addsf  28175  negsf  28245  noseqind  28485  vtxdgfisf  29826  hlimf  31589  pjrni  32054  pjmf1  32068  2ndresdju  32994  nsgmgc  33721  selvply1rhmlemb  33909  mplvrpmrhm  33937  reprinfz1  35009  reprdifc  35014  bnj149  35263  subfacp1lem3  35674  mrsubrn  36005  msrf  36034  mclsind  36062  neibastop2lem  36891  weiunlem  36994  mh-inf3f1  37072  rrncmslem  38503  cdlemk56  41765  sticksstones22  42955  hbtlem7  43872  dgraaf  43894  deg1mhm  43947  elixpconstg  45827  elmapsnd  45941  unirnmap  45944  resincncf  46609  dvnprodlem1  46680  volioof  46721  voliooicof  46730  qndenserrnbllem  47028  subsaliuncllem  47091  fge0iccico  47104  elhoi  47276  ovnsubaddlem1  47304  hoiqssbllem3  47358  ovolval4lem1  47383  rrx2xpref1o  49518  oppff1  49946  fucofulem2  50109