This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )