Description: The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fmptssfisupp.1 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) finSupp 𝑍 ) | |
fmptssfisupp.2 | ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 ) | ||
fmptssfisupp.3 | ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 ) | ||
Assertion | fmptssfisupp | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) finSupp 𝑍 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmptssfisupp.1 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) finSupp 𝑍 ) | |
2 | fmptssfisupp.2 | ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 ) | |
3 | fmptssfisupp.3 | ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 ) | |
4 | 2 | resmptd | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) |
5 | 1 3 | fsuppres | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) finSupp 𝑍 ) |
6 | 4 5 | eqbrtrrd | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) finSupp 𝑍 ) |