Theorem ffnfv 7119

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 6709	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		ffvelcdm 7081	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
3	2	ralrimiva 3155	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)
4	1, 3	jca 521	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5		simpl 488	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴)
6		fvelrnb 6945	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
7	6	biimpd 232	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦))
8		nfra1 3287	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵
9		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
10		rsp 3251	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵))
11		eleq1 2849	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
12	11	biimpcd 252	. . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
13	10, 12	syl6 36	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)))
14	8, 9, 13	rexlimd 3270	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))
15	7, 14	sylan9 517	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵))
16	15	ssrdv 3937	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)
17		df-f 6542	. . 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 3077  ∃wrex 3087   ⊆ wss 3899  ran crn 5652   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  ffnfvf  7120  fnfvrnss  7121  fcdmssb  7122  fmpt2d  7125  fssrescdmd  7127  fconstfv  7218  ffnov  7546  seqomlem2  8461  naddf  8691  elixpconst  8933  elixpsn  8965  unblem4  9287  ordtypelem4  9515  oismo  9534  cantnfvalf  9666  rankf  9802  alephon  10148  alephf1  10164  alephf1ALT  10182  alephfplem4  10186  cfsmolem  10348  infpssrlem3  10383  axcc4  10517  domtriomlem  10520  pwfseqlem3  10745  gch3  10761  inar1  10860  peano5nni  12338  cnref1o  13113  seqf2  14164  hashkf  14476  iswrdsymb  14676  ccatrn  14735  shftf  15232  sqrtf  15531  isercoll2  15836  eff2  16267  reeff1  16288  1arith  17105  ramcl  17207  xpscf  17737  dmaf  18224  cdaf  18225  coapm  18246  odf  19751  gsumpt  20176  dprdff  20228  dprdfcntz  20231  dprdfadd  20236  dprdlub  20242  rngmgpf  20379  mgpf  20475  prdscrngd  20551  isabvd  21069  psgnghm  21886  frlmsslsp  22102  psrbagcon  22233  mvrf2  22300  subrgmvrf  22343  mplbas2  22351  kqf  24066  fmf  24264  tmdgsum2  24415  prdstmdd  24443  prdstgpd  24444  prdsxmslem2  24848  metdsre  25173  evth  25280  evthicc2  25781  ovolfsf  25792  ovolf  25803  vitalilem2  25930  vitalilem5  25933  0plef  25993  mbfi1fseqlem4  26039  xrge0f  26052  itg2addlem  26079  dvfre  26271  dvne0  26331  mdegxrf  26386  mtest  26731  psercn  26753  recosf1o  26863  logcn  26975  amgm  27318  emcllem7  27329  dchrfi  27582  dchr1re  27590  dchrisum0re  27840  padicabvf  27958  addsf  28368  negsf  28438  noseqind  28678  vtxdgfisf  30057  hlimf  31839  pjrni  32304  pjmf1  32318  2ndresdju  33243  nsgmgc  33963  selvply1rhmlemb  34151  mplvrpmrhm  34179  reprinfz1  35251  reprdifc  35256  bnj149  35505  subfacp1lem3  35947  mrsubrn  36278  msrf  36307  mclsind  36335  neibastop2lem  37148  weiunlem  37251  mh-inf3f1  37329  rrncmslem  38766  cdlemk56  42028  sticksstones22  43218  hbtlem7  44126  dgraaf  44148  deg1mhm  44201  elixpconstg  46103  elmapsnd  46217  unirnmap  46220  resincncf  46884  dvnprodlem1  46955  volioof  46996  voliooicof  47005  qndenserrnbllem  47303  subsaliuncllem  47366  fge0iccico  47379  elhoi  47551  ovnsubaddlem1  47579  hoiqssbllem3  47633  ovolval4lem1  47658  rrx2xpref1o  49829  oppff1  50255  fucofulem2  50418