Metamath Proof Explorer

Theorem psrbag

Description: Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion psrbag ⊢ I ∈ V → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 cnveq ⊢ f = F → f -1 = F -1
3 2 imaeq1d ⊢ f = F → f -1 ℕ = F -1 ℕ
4 3 eleq1d ⊢ f = F → f -1 ℕ ∈ Fin ↔ F -1 ℕ ∈ Fin
5 4 1 elrab2 ⊢ F ∈ D ↔ F ∈ ℕ 0 I ∧ F -1 ℕ ∈ Fin
6 nn0ex ⊢ ℕ 0 ∈ V
7 elmapg ⊢ ℕ 0 ∈ V ∧ I ∈ V → F ∈ ℕ 0 I ↔ F : I ⟶ ℕ 0
8 6 7 mpan ⊢ I ∈ V → F ∈ ℕ 0 I ↔ F : I ⟶ ℕ 0
9 8 anbi1d ⊢ I ∈ V → F ∈ ℕ 0 I ∧ F -1 ℕ ∈ Fin ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
10 5 9 bitrid ⊢ I ∈ V → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin