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 ) ) )