Metamath Proof Explorer


Theorem offinsupp1

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

Ref Expression
Hypotheses offinsupp1.a ( 𝜑𝐴𝑉 )
offinsupp1.y ( 𝜑𝑌𝑈 )
offinsupp1.z ( 𝜑𝑍𝑊 )
offinsupp1.f ( 𝜑𝐹 : 𝐴𝑆 )
offinsupp1.g ( 𝜑𝐺 : 𝐴𝑇 )
offinsupp1.1 ( 𝜑𝐹 finSupp 𝑌 )
offinsupp1.2 ( ( 𝜑𝑥𝑇 ) → ( 𝑌 𝑅 𝑥 ) = 𝑍 )
Assertion offinsupp1 ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 offinsupp1.a ( 𝜑𝐴𝑉 )
2 offinsupp1.y ( 𝜑𝑌𝑈 )
3 offinsupp1.z ( 𝜑𝑍𝑊 )
4 offinsupp1.f ( 𝜑𝐹 : 𝐴𝑆 )
5 offinsupp1.g ( 𝜑𝐺 : 𝐴𝑇 )
6 offinsupp1.1 ( 𝜑𝐹 finSupp 𝑌 )
7 offinsupp1.2 ( ( 𝜑𝑥𝑇 ) → ( 𝑌 𝑅 𝑥 ) = 𝑍 )
8 6 fsuppimpd ( 𝜑 → ( 𝐹 supp 𝑌 ) ∈ Fin )
9 ssidd ( 𝜑 → ( 𝐹 supp 𝑌 ) ⊆ ( 𝐹 supp 𝑌 ) )
10 9 7 4 5 1 2 suppssof1 ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑌 ) )
11 8 10 ssfid ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin )
12 ovexd ( ( 𝜑 ∧ ( 𝑖𝑆𝑗𝑇 ) ) → ( 𝑖 𝑅 𝑗 ) ∈ V )
13 inidm ( 𝐴𝐴 ) = 𝐴
14 12 4 5 1 1 13 off ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) : 𝐴 ⟶ V )
15 14 ffund ( 𝜑 → Fun ( 𝐹f 𝑅 𝐺 ) )
16 ovexd ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) ∈ V )
17 funisfsupp ( ( Fun ( 𝐹f 𝑅 𝐺 ) ∧ ( 𝐹f 𝑅 𝐺 ) ∈ V ∧ 𝑍𝑊 ) → ( ( 𝐹f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) )
18 15 16 3 17 syl3anc ( 𝜑 → ( ( 𝐹f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) )
19 11 18 mpbird ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) finSupp 𝑍 )