This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ℕ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 }