Metamath Proof Explorer


Theorem psrbagfOLD

Description: Obsolete version of psrbag as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagfOLD ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 1 psrbag ( 𝐼𝑉 → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
3 2 simprbda ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )