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 1 𝑜 = f ∈ ℕ 0 1 𝑜 | f -1 ℕ ∈ Fin

Proof

Step Hyp Ref Expression
1 rabid2 ⊢ ℕ 0 1 𝑜 = f ∈ ℕ 0 1 𝑜 | f -1 ℕ ∈ Fin ↔ ∀ f ∈ ℕ 0 1 𝑜 f -1 ℕ ∈ Fin
2 df1o2 ⊢ 1 𝑜 = ∅
3 snfi ⊢ ∅ ∈ Fin
4 2 3 eqeltri ⊢ 1 𝑜 ∈ Fin
5 cnvimass ⊢ f -1 ℕ ⊆ dom ⁡ f
6 elmapi ⊢ f ∈ ℕ 0 1 𝑜 → f : 1 𝑜 ⟶ ℕ 0
7 5 6 fssdm ⊢ f ∈ ℕ 0 1 𝑜 → f -1 ℕ ⊆ 1 𝑜
8 ssfi ⊢ 1 𝑜 ∈ Fin ∧ f -1 ℕ ⊆ 1 𝑜 → f -1 ℕ ∈ Fin
9 4 7 8 sylancr ⊢ f ∈ ℕ 0 1 𝑜 → f -1 ℕ ∈ Fin
10 1 9 mprgbir ⊢ ℕ 0 1 𝑜 = f ∈ ℕ 0 1 𝑜 | f -1 ℕ ∈ Fin