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

Metamath Proof Explorer

Theorem ressuppfi

Description: If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019)

Ref Expression
Hypotheses ressuppfi.b ⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
ressuppfi.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
ressuppfi.g ⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
ressuppfi.s ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
ressuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion ressuppfi ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 ressuppfi.b ⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
2 ressuppfi.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
3 ressuppfi.g ⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
4 ressuppfi.s ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
5 ressuppfi.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
6 3 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) = 𝐺 )
7 6 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = ( 𝐺 supp 𝑍 ) )
8 7 4 eqeltrd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∈ Fin )
9 unfi ⊢ ( ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∈ Fin ∧ ( dom 𝐹 ∖ 𝐵 ) ∈ Fin ) → ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) ∈ Fin )
10 8 1 9 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) ∈ Fin )
11 ressuppssdif ⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
12 2 5 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
13 10 12 ssfid ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )