Theorem ffnfv 7101

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 6692	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7063	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3155	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 519	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 486	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6928	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 231	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3287	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1935	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3251	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2851	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 251	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3270	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 515	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3943	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6526	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 592	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 211	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ∀wral 3077  ∃wrex 3087   ⊆ wss 3905  ran crn 5649   Fn wfn 6517  ⟶wf 6518  ‘cfv 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-fv 6530

This theorem is referenced by:  ffnfvf  7102  fnfvrnss  7103  fcdmssb  7104  fmpt2d  7107  fssrescdmd  7109  fconstfv  7197  ffnov  7523  seqomlem2  8423  naddf  8653  elixpconst  8888  elixpsn  8920  unblem4  9240  ordtypelem4  9470  oismo  9489  cantnfvalf  9621  rankf  9753  alephon  10026  alephf1  10042  alephf1ALT  10060  alephfplem4  10064  cfsmolem  10228  infpssrlem3  10263  axcc4  10397  domtriomlem  10400  pwfseqlem3  10619  gch3  10635  inar1  10734  peano5nni  12214  cnref1o  12987  seqf2  14035  hashkf  14346  iswrdsymb  14545  ccatrn  14604  shftf  15093  sqrtf  15392  isercoll2  15697  eff2  16132  reeff1  16153  1arith  16964  ramcl  17066  xpscf  17596  dmaf  18083  cdaf  18084  coapm  18105  odf  19578  gsumpt  20003  dprdff  20055  dprdfcntz  20058  dprdfadd  20063  dprdlub  20069  rngmgpf  20204  mgpf  20299  prdscrngd  20371  isabvd  20862  psgnghm  21633  frlmsslsp  21849  psrbagcon  21978  mvrf2  22045  subrgmvrf  22088  mplbas2  22096  kqf  23808  fmf  24006  tmdgsum2  24157  prdstmdd  24185  prdstgpd  24186  prdsxmslem2  24590  metdsre  24915  evth  25022  evthicc2  25523  ovolfsf  25534  ovolf  25545  vitalilem2  25672  vitalilem5  25675  0plef  25735  mbfi1fseqlem4  25781  xrge0f  25794  itg2addlem  25821  dvfre  26014  dvne0  26074  mdegxrf  26129  mtest  26468  psercn  26490  recosf1o  26601  logcn  26713  amgm  27056  emcllem7  27067  dchrfi  27320  dchr1re  27328  dchrisum0re  27578  padicabvf  27696  addsf  28076  negsf  28146  noseqind  28386  vtxdgfisf  29678  hlimf  31441  pjrni  31906  pjmf1  31920  2ndresdju  32852  nsgmgc  33599  selvply1rhmlemb  33817  mplvrpmrhm  33845  reprinfz1  34917  reprdifc  34922  bnj149  35171  subfacp1lem3  35533  mrsubrn  35864  msrf  35893  mclsind  35921  neibastop2lem  36721  weiunlem  36824  mh-inf3f1  36902  rrncmslem  38332  cdlemk56  41596  sticksstones22  42786  hbtlem7  43703  dgraaf  43725  deg1mhm  43778  elixpconstg  45668  elmapsnd  45782  unirnmap  45785  resincncf  46450  dvnprodlem1  46521  volioof  46562  voliooicof  46571  qndenserrnbllem  46869  subsaliuncllem  46932  fge0iccico  46945  elhoi  47117  ovnsubaddlem1  47145  hoiqssbllem3  47199  ovolval4lem1  47224  rrx2xpref1o  49341  oppff1  49770  fucofulem2  49933