Theorem psrbagfsuppOLD

Description: Obsolete version of psrbagfsupp as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	psrbagfsuppOLD	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → 𝑋 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2	1	psrbag	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑋 “ ℕ ) ∈ Fin ) ) )
3	2	biimpac	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑋 “ ℕ ) ∈ Fin ) )
4	3	simprd	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → ( ◡ 𝑋 “ ℕ ) ∈ Fin )
5		simpr	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
6	1	psrbagfOLD	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
7	6	ancoms	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
8		frnnn0fsupp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ) → ( 𝑋 finSupp 0 ↔ ( ◡ 𝑋 “ ℕ ) ∈ Fin ) )
9	5 7 8	syl2anc	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑋 finSupp 0 ↔ ( ◡ 𝑋 “ ℕ ) ∈ Fin ) )
10	4 9	mpbird	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝐼 ∈ 𝑉 ) → 𝑋 finSupp 0 )