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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbag ( 𝐼𝑉 → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 cnveq ( 𝑓 = 𝐹 𝑓 = 𝐹 )
3 2 imaeq1d ( 𝑓 = 𝐹 → ( 𝑓 “ ℕ ) = ( 𝐹 “ ℕ ) )
4 3 eleq1d ( 𝑓 = 𝐹 → ( ( 𝑓 “ ℕ ) ∈ Fin ↔ ( 𝐹 “ ℕ ) ∈ Fin ) )
5 4 1 elrab2 ( 𝐹𝐷 ↔ ( 𝐹 ∈ ( ℕ0m 𝐼 ) ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
6 nn0ex 0 ∈ V
7 elmapg ( ( ℕ0 ∈ V ∧ 𝐼𝑉 ) → ( 𝐹 ∈ ( ℕ0m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ ℕ0 ) )
8 6 7 mpan ( 𝐼𝑉 → ( 𝐹 ∈ ( ℕ0m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ ℕ0 ) )
9 8 anbi1d ( 𝐼𝑉 → ( ( 𝐹 ∈ ( ℕ0m 𝐼 ) ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
10 5 9 syl5bb ( 𝐼𝑉 → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )