offinsupp1

Description: Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023)

Step	Hyp	Ref	Expression
1		offinsupp1.a	$⊢ φ \to A \in V$
2		offinsupp1.y	$⊢ φ \to Y \in U$
3		offinsupp1.z	$⊢ φ \to Z \in W$
4		offinsupp1.f	$⊢ φ \to F : A ⟶ S$
5		offinsupp1.g	$⊢ φ \to G : A ⟶ T$
6		offinsupp1.1	$⊢ φ \to {finSupp}_{Y} (F)$
7		offinsupp1.2	$⊢ (φ \land x \in T) \to Y R x = Z$
8	6	fsuppimpd	$⊢ φ \to F supp Y \in Fin$
9		ssidd	$⊢ φ \to F supp Y \subseteq F supp Y$
10	9 7 4 5 1 2	suppssof1	$⊢ φ \to (F R_{f} G) supp Z \subseteq F supp Y$
11	8 10	ssfid	$⊢ φ \to (F R_{f} G) supp Z \in Fin$
12		ovexd	$⊢ (φ \land (i \in S \land j \in T)) \to i R j \in V$
13		inidm	$⊢ A \cap A = A$
14	12 4 5 1 1 13	off	$⊢ φ \to (F R_{f} G) : A ⟶ V$
15	14	ffund	$⊢ φ \to Fun (F R_{f} G)$
16		ovexd	$⊢ φ \to F R_{f} G \in V$
17		funisfsupp	$⊢ (Fun (F R_{f} G) \land F R_{f} G \in V \land Z \in W) \to ({finSupp}_{Z} ((F R_{f} G)) \leftrightarrow (F R_{f} G) supp Z \in Fin)$
18	15 16 3 17	syl3anc	$⊢ φ \to ({finSupp}_{Z} ((F R_{f} G)) \leftrightarrow (F R_{f} G) supp Z \in Fin)$
19	11 18	mpbird	$⊢ φ \to {finSupp}_{Z} ((F R_{f} G))$

Metamath Proof Explorer