Theorem ffnfv 7113

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 6703	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7075	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3154	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 521	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 488	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6939	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3286	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3250	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2848	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3269	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 517	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3937	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6537	. . 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 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086   ⊆ wss 3899  ran crn 5656   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541

This theorem is used by:  ffnfvf  7114  fnfvrnss  7115  fcdmssb  7116  fmpt2d  7119  fssrescdmd  7121  fconstfv  7212  ffnov  7540  seqomlem2  8443  naddf  8673  elixpconst  8915  elixpsn  8947  unblem4  9268  ordtypelem4  9496  oismo  9515  cantnfvalf  9647  rankf  9779  alephon  10075  alephf1  10091  alephf1ALT  10109  alephfplem4  10113  cfsmolem  10275  infpssrlem3  10310  axcc4  10444  domtriomlem  10447  pwfseqlem3  10672  gch3  10688  inar1  10787  peano5nni  12263  cnref1o  13038  seqf2  14088  hashkf  14399  iswrdsymb  14599  ccatrn  14658  shftf  15155  sqrtf  15454  isercoll2  15759  eff2  16190  reeff1  16211  1arith  17022  ramcl  17124  xpscf  17654  dmaf  18141  cdaf  18142  coapm  18163  odf  19667  gsumpt  20092  dprdff  20144  dprdfcntz  20147  dprdfadd  20152  dprdlub  20158  rngmgpf  20295  mgpf  20390  prdscrngd  20465  isabvd  20981  psgnghm  21796  frlmsslsp  22012  psrbagcon  22143  mvrf2  22210  subrgmvrf  22253  mplbas2  22261  kqf  23976  fmf  24174  tmdgsum2  24325  prdstmdd  24353  prdstgpd  24354  prdsxmslem2  24758  metdsre  25083  evth  25190  evthicc2  25691  ovolfsf  25702  ovolf  25713  vitalilem2  25840  vitalilem5  25843  0plef  25903  mbfi1fseqlem4  25949  xrge0f  25962  itg2addlem  25989  dvfre  26181  dvne0  26241  mdegxrf  26296  mtest  26643  psercn  26665  recosf1o  26775  logcn  26887  amgm  27230  emcllem7  27241  dchrfi  27494  dchr1re  27502  dchrisum0re  27752  padicabvf  27870  addsf  28250  negsf  28320  noseqind  28560  vtxdgfisf  29939  hlimf  31721  pjrni  32186  pjmf1  32200  2ndresdju  33125  nsgmgc  33844  selvply1rhmlemb  34032  mplvrpmrhm  34060  reprinfz1  35133  reprdifc  35138  bnj149  35387  subfacp1lem3  35764  mrsubrn  36095  msrf  36124  mclsind  36152  neibastop2lem  36982  weiunlem  37085  mh-inf3f1  37163  rrncmslem  38585  cdlemk56  41847  sticksstones22  43037  hbtlem7  43969  dgraaf  43991  deg1mhm  44044  elixpconstg  45924  elmapsnd  46038  unirnmap  46041  resincncf  46706  dvnprodlem1  46777  volioof  46818  voliooicof  46827  qndenserrnbllem  47125  subsaliuncllem  47188  fge0iccico  47201  elhoi  47373  ovnsubaddlem1  47401  hoiqssbllem3  47455  ovolval4lem1  47480  rrx2xpref1o  49651  oppff1  50077  fucofulem2  50240