Theorem psrbagf 22233

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 2852	. 2 ⊢ (𝐹 ∈ 𝐷 ↔ 𝐹 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
3		elrabi 3640	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝐹 ∈ (ℕ0 ↑m 𝐼))
4		elmapi 8874	. . 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 1569   ∈ wcel 2144  {crab 3412  ^◡ccnv 5649   “ cima 5653  ⟶wf 6537  (class class class)co 7422   ↑_m cmap 8852  Fincfn 8978  ℕcn 12340  ℕ₀cn0 12611

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7425  df-oprab 7426  df-mpo 7427  df-1st 8003  df-2nd 8004  df-map 8854

This theorem is used by:  psrbagfsupp  22234  psrbaglesupp  22237  psrbaglecl  22238  psrbagaddcl  22239  psrbagcon  22240  psrbaglefi  22241  psrbagconcl  22242  psrbagleadd1  22243  psrbagconf1o  22244  psrbagres  22245  gsumbagdiaglem  22246  psrass1lem  22248  rhmpsrlem2  22256  psrlidm  22276  psrridm  22277  psrass1  22278  psrcom  22282  mplsubrglem  22318  mplmonmul  22352  psrbagev1  22393  evlslem3  22396  evlslem1  22398  evlsvvvallem  22407  evlsvvval  22409  selvvvval  22458  mhpmulcl  22477  psdcl  22489  psdmplcl  22490  psdadd  22491  psdvsca  22492  psdmul  22494  psdmvr  22497  psropprmul  22562  tdeglem1  26383  tdeglem3  26384  tdeglem4  26385  mdegmullem  26403  mplvrpmfgalem  34224  psrmonmul  34230  evlselvlem  43723  evlselv  43724  mhphflem  43731  mhphf  43732