Theorem frnnn0fsuppg

Description: Version of frnnn0fsupp avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 5-Aug-2024)

	Ref	Expression
Assertion	frnnn0fsuppg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		ffun	⊢ ( 𝐹 : 𝐼 ⟶ ℕ0 → Fun 𝐹 )
2		simpl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → 𝐹 ∈ 𝑉 )
3		c0ex	⊢ 0 ∈ V
4		funisfsupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
5	3 4	mp3an3	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
6	1 2 5	syl2an2	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( 𝐹 supp 0 ) ∈ Fin ) )
7		frnnn0suppg	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
8	7	eleq1d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( ( 𝐹 supp 0 ) ∈ Fin ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
9	6 8	bitrd	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 finSupp 0 ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )