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	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to ({finSupp}_{0} (F) \leftrightarrow F^{-1} [ℕ] \in Fin)$

Step	Hyp	Ref	Expression
1		ffun	$⊢ F : I ⟶ ℕ_{0} \to Fun F$
2		simpl	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to F \in V$
3		c0ex	$⊢ 0 \in V$
4		funisfsupp	$⊢ (Fun F \land F \in V \land 0 \in V) \to ({finSupp}_{0} (F) \leftrightarrow F supp 0 \in Fin)$
5	3 4	mp3an3	$⊢ (Fun F \land F \in V) \to ({finSupp}_{0} (F) \leftrightarrow F supp 0 \in Fin)$
6	1 2 5	syl2an2	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to ({finSupp}_{0} (F) \leftrightarrow F supp 0 \in Fin)$
7		frnnn0suppg	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to F supp 0 = F^{-1} [ℕ]$
8	7	eleq1d	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to (F supp 0 \in Fin \leftrightarrow F^{-1} [ℕ] \in Fin)$
9	6 8	bitrd	$⊢ (F \in V \land F : I ⟶ ℕ_{0}) \to ({finSupp}_{0} (F) \leftrightarrow F^{-1} [ℕ] \in Fin)$

Metamath Proof Explorer