Metamath Proof Explorer


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 ( ℕ0m 1o ) = { 𝑓 ∈ ( ℕ0m 1o ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }

Proof

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