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

Metamath Proof Explorer

Theorem resfifsupp

Description: The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019)

Ref Expression
Hypotheses resfifsupp.f ⊢ ( 𝜑 → Fun 𝐹 )
resfifsupp.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
resfifsupp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion resfifsupp ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 resfifsupp.f ⊢ ( 𝜑 → Fun 𝐹 )
2 resfifsupp.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 resfifsupp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
4 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
5 1 4 syl ⊢ ( 𝜑 → Rel 𝐹 )
6 resindm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑋 ) )
7 5 6 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑋 ) )
8 1 funfnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
9 fnresin2 ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) Fn ( 𝑋 ∩ dom 𝐹 ) )
11 infi ⊢ ( 𝑋 ∈ Fin → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
12 2 11 syl ⊢ ( 𝜑 → ( 𝑋 ∩ dom 𝐹 ) ∈ Fin )
13 10 12 3 fndmfifsupp ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 ∩ dom 𝐹 ) ) finSupp 𝑍 )
14 7 13 eqbrtrrd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑋 ) finSupp 𝑍 )