Theorem offinsupp1

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

	Ref	Expression
Hypotheses	offinsupp1.a	|- ( ph -> A e. V )
	offinsupp1.y	|- ( ph -> Y e. U )
	offinsupp1.z	|- ( ph -> Z e. W )
	offinsupp1.f	|- ( ph -> F : A --> S )
	offinsupp1.g	|- ( ph -> G : A --> T )
	offinsupp1.1	|- ( ph -> F finSupp Y )
	offinsupp1.2	|- ( ( ph /\ x e. T ) -> ( Y R x ) = Z )
Assertion	offinsupp1	|- ( ph -> ( F oF R G ) finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		offinsupp1.a	|- ( ph -> A e. V )
2		offinsupp1.y	|- ( ph -> Y e. U )
3		offinsupp1.z	|- ( ph -> Z e. W )
4		offinsupp1.f	|- ( ph -> F : A --> S )
5		offinsupp1.g	|- ( ph -> G : A --> T )
6		offinsupp1.1	|- ( ph -> F finSupp Y )
7		offinsupp1.2	|- ( ( ph /\ x e. T ) -> ( Y R x ) = Z )
8	6	fsuppimpd	|- ( ph -> ( F supp Y ) e. Fin )
9		ssidd	|- ( ph -> ( F supp Y ) C_ ( F supp Y ) )
10	9 7 4 5 1 2	suppssof1	|- ( ph -> ( ( F oF R G ) supp Z ) C_ ( F supp Y ) )
11	8 10	ssfid	|- ( ph -> ( ( F oF R G ) supp Z ) e. Fin )
12		ovexd	|- ( ( ph /\ ( i e. S /\ j e. T ) ) -> ( i R j ) e. _V )
13		inidm	|- ( A i^i A ) = A
14	12 4 5 1 1 13	off	|- ( ph -> ( F oF R G ) : A --> _V )
15	14	ffund	|- ( ph -> Fun ( F oF R G ) )
16		ovexd	|- ( ph -> ( F oF R G ) e. _V )
17		funisfsupp	|- ( ( Fun ( F oF R G ) /\ ( F oF R G ) e. _V /\ Z e. W ) -> ( ( F oF R G ) finSupp Z <-> ( ( F oF R G ) supp Z ) e. Fin ) )
18	15 16 3 17	syl3anc	|- ( ph -> ( ( F oF R G ) finSupp Z <-> ( ( F oF R G ) supp Z ) e. Fin ) )
19	11 18	mpbird	|- ( ph -> ( F oF R G ) finSupp Z )