ffsuppbi

Description: Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019)

		Ref	Expression
	Assertion	ffsuppbi	$⊢ (I \in V \land Z \in W) \to (F : I ⟶ S \to ({finSupp}_{Z} (F) \leftrightarrow F^{-1} [S ∖ \{Z\}] \in Fin))$

Step	Hyp	Ref	Expression
1		ffun	$⊢ F : I ⟶ S \to Fun F$
2	1	adantl	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to Fun F$
3		fex	$⊢ (F : I ⟶ S \land I \in V) \to F \in V$
4	3	expcom	$⊢ I \in V \to (F : I ⟶ S \to F \in V)$
5	4	adantr	$⊢ (I \in V \land Z \in W) \to (F : I ⟶ S \to F \in V)$
6	5	imp	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to F \in V$
7		simplr	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to Z \in W$
8		funisfsupp	$⊢ (Fun F \land F \in V \land Z \in W) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
9	2 6 7 8	syl3anc	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
10		fsuppeq	$⊢ (I \in V \land Z \in W) \to (F : I ⟶ S \to F supp Z = F^{-1} [S ∖ \{Z\}])$
11	10	imp	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to F supp Z = F^{-1} [S ∖ \{Z\}]$
12	11	eleq1d	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to (F supp Z \in Fin \leftrightarrow F^{-1} [S ∖ \{Z\}] \in Fin)$
13	9 12	bitrd	$⊢ ((I \in V \land Z \in W) \land F : I ⟶ S) \to ({finSupp}_{Z} (F) \leftrightarrow F^{-1} [S ∖ \{Z\}] \in Fin)$
14	13	ex	$⊢ (I \in V \land Z \in W) \to (F : I ⟶ S \to ({finSupp}_{Z} (F) \leftrightarrow F^{-1} [S ∖ \{Z\}] \in Fin))$

Metamath Proof Explorer