Theorem ffnfv 6642

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 6282	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelrn 6611	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3175	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 507	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 476	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6494	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 221	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3150	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 2013	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3138	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2894	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 241	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3235	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 503	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3833	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6131	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
18	5, 16, 17	sylanbrc 578	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵)
19	4, 18	impbii 201	1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∀wral 3117  ∃wrex 3118   ⊆ wss 3798  ran crn 5347   Fn wfn 6122  ⟶wf 6123  ‘cfv 6127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pr 5129

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-fv 6135

This theorem is referenced by:  ffnfvf  6643  fnfvrnss  6644  frnssb  6645  fmpt2d  6647  fconstfv  6737  ffnov  7029  seqomlem2  7817  elixpconst  8189  elixpsn  8220  unblem4  8490  ordtypelem4  8702  oismo  8721  cantnfvalf  8846  rankf  8941  alephon  9212  alephf1  9228  alephf1ALT  9246  alephfplem4  9250  cfsmolem  9414  infpssrlem3  9449  axcc4  9583  domtriomlem  9586  axdclem2  9664  pwfseqlem3  9804  gch3  9820  inar1  9919  peano5nni  11360  cnref1o  12114  seqf2  13121  hashkf  13419  iswrdsymb  13598  ccatrn  13656  shftf  14203  sqrtf  14487  isercoll2  14783  eff2  15208  reeff1  15229  1arith  16009  ramcl  16111  xpscf  16586  dmaf  17058  cdaf  17059  coapm  17080  odf  18314  gsumpt  18721  dprdff  18772  dprdfcntz  18775  dprdfadd  18780  dprdlub  18786  mgpf  18920  prdscrngd  18974  isabvd  19183  psrbagcon  19739  subrgmvrf  19830  mplbas2  19838  mvrf2  19859  psgnghm  20292  frlmsslsp  20509  kqf  21928  fmf  22126  tmdgsum2  22277  prdstmdd  22304  prdstgpd  22305  prdsxmslem2  22711  metdsre  23033  evth  23135  evthicc2  23633  ovolfsf  23644  ovolf  23655  vitalilem2  23782  vitalilem5  23785  0plef  23845  mbfi1fseqlem4  23891  xrge0f  23904  itg2addlem  23931  dvfre  24120  dvne0  24180  mdegxrf  24234  mtest  24564  psercn  24586  recosf1o  24688  logcn  24799  amgm  25137  emcllem7  25148  dchrfi  25400  dchr1re  25408  dchrisum0re  25622  padicabvf  25740  vtxdgfisf  26781  wlkresOLD  26978  hlimf  28645  pjrni  29112  pjmf1  29126  reprinfz1  31245  reprdifc  31250  bnj149  31487  subfacp1lem3  31706  mrsubrn  31952  msrf  31981  mclsind  32009  neibastop2lem  32888  rrncmslem  34168  cdlemk56  37041  hbtlem7  38533  dgraaf  38555  deg1mhm  38623  elixpconstg  40078  elmapsnd  40197  unirnmap  40201  resincncf  40877  dvnprodlem1  40950  volioof  40992  voliooicof  41001  qndenserrnbllem  41299  subsaliuncllem  41360  fge0iccico  41372  elhoi  41544  ovnsubaddlem1  41572  hoiqssbllem3  41626  ovolval4lem1  41651  rrx2xpref1o  42276