Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finitely supported functions
resfsupp
Metamath Proof Explorer
Description: If the restriction of a function by a set which, subtracted from the
domain of the function so that its difference is finitely supported, the
function itself is finitely supported. (Contributed by AV , 27-May-2019)
Ref
Expression
Hypotheses
resfsupp.b
⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
resfsupp.e
⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
resfsupp.f
⊢ ( 𝜑 → Fun 𝐹 )
resfsupp.g
⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
resfsupp.s
⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
resfsupp.z
⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion
resfsupp
⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Proof
Step
Hyp
Ref
Expression
1
resfsupp.b
⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
2
resfsupp.e
⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
3
resfsupp.f
⊢ ( 𝜑 → Fun 𝐹 )
4
resfsupp.g
⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
5
resfsupp.s
⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
6
resfsupp.z
⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
7
5
fsuppimpd
⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
8
1 2 4 7 6
ressuppfi
⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
9
funisfsupp
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
10
3 2 6 9
syl3anc
⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
11
8 10
mpbird
⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )