Theorem psr1baslem

Description: The set of finite bags on 1o is just the set of all functions from 1o to NN0 . (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Assertion	psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }

Proof

Step	Hyp	Ref	Expression
1		rabid2	⊢ ( ( ℕ0 ↑m 1o ) = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↔ ∀ 𝑓 ∈ ( ℕ0 ↑m 1o ) ( ◡ 𝑓 “ ℕ ) ∈ Fin )
2		df1o2	⊢ 1o = { ∅ }
3		snfi	⊢ { ∅ } ∈ Fin
4	2 3	eqeltri	⊢ 1o ∈ Fin
5		cnvimass	⊢ ( ◡ 𝑓 “ ℕ ) ⊆ dom 𝑓
6		elmapi	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → 𝑓 : 1o ⟶ ℕ0 )
7	5 6	fssdm	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → ( ◡ 𝑓 “ ℕ ) ⊆ 1o )
8		ssfi	⊢ ( ( 1o ∈ Fin ∧ ( ◡ 𝑓 “ ℕ ) ⊆ 1o ) → ( ◡ 𝑓 “ ℕ ) ∈ Fin )
9	4 7 8	sylancr	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → ( ◡ 𝑓 “ ℕ ) ∈ Fin )
10	1 9	mprgbir	⊢ ( ℕ0 ↑m 1o ) = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }