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

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

Proof

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