Theorem psrbagf 22098

Description: A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.)

Hypothesis

Ref	Expression
psrbag.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}

Assertion

Ref	Expression
psrbagf	⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0)

Distinct variable groups:   𝑓,𝐹   𝑓,𝐼

Allowed substitution hint:   𝐷(𝑓)

Proof of Theorem psrbagf

Step	Hyp	Ref	Expression
1		psrbag.d	. . 3 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
2	1	eleq2i 2857	. 2 ⊢ (𝐹 ∈ 𝐷 ↔ 𝐹 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
3		elrabi 3648	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝐹 ∈ (ℕ0 ↑m 𝐼))
4		elmapi 8848	. . 3 ⊢ (𝐹 ∈ (ℕ0 ↑m 𝐼) → 𝐹:𝐼⟶ℕ0)
5	3, 4	syl 18	. 2 ⊢ (𝐹 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝐹:𝐼⟶ℕ0)
6	2, 5	sylbi 220	1 ⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3418  ^◡ccnv 5662   “ cima 5666  ⟶wf 6536  (class class class)co 7416   ↑_m cmap 8826  Fincfn 8945  ℕcn 12244  ℕ₀cn0 12515

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7988  df-2nd 7989  df-map 8828

This theorem is used by:  psrbagfsupp  22099  psrbaglesupp  22102  psrbaglecl  22103  psrbagaddcl  22104  psrbagcon  22105  psrbaglefi  22106  psrbagconcl  22107  psrbagleadd1  22108  psrbagconf1o  22109  psrbagres  22110  gsumbagdiaglem  22111  psrass1lem  22113  rhmpsrlem2  22121  psrlidm  22141  psrridm  22142  psrass1  22143  psrcom  22147  mplsubrglem  22183  mplmonmul  22217  psrbagev1  22258  evlslem3  22261  evlslem1  22263  evlsvvvallem  22272  evlsvvval  22274  selvvvval  22323  mhpmulcl  22342  psdcl  22354  psdmplcl  22355  psdadd  22356  psdvsca  22357  psdmul  22359  psdmvr  22362  psropprmul  22427  tdeglem1  26246  tdeglem3  26247  tdeglem4  26248  mdegmullem  26266  mplvrpmfgalem  33974  psrmonmul  33980  evlselvlem  43353  evlselv  43354  mhphflem  43361  mhphf  43362