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

Metamath Proof Explorer

Theorem fsuppss

Description: A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypotheses fsuppss.1 ⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
fsuppss.2 ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
Assertion fsuppss ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fsuppss.1 ⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
2 fsuppss.2 ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
3 relfsupp ⊢ Rel finSupp
4 brrelex1 ⊢ ( ( Rel finSupp ∧ 𝐺 finSupp 𝑍 ) → 𝐺 ∈ V )
5 3 2 4 sylancr ⊢ ( 𝜑 → 𝐺 ∈ V )
6 5 1 ssexd ⊢ ( 𝜑 → 𝐹 ∈ V )
7 brrelex2 ⊢ ( ( Rel finSupp ∧ 𝐺 finSupp 𝑍 ) → 𝑍 ∈ V )
8 3 2 7 sylancr ⊢ ( 𝜑 → 𝑍 ∈ V )
9 2 fsuppfund ⊢ ( 𝜑 → Fun 𝐺 )
10 funss ⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐺 → Fun 𝐹 ) )
11 1 9 10 sylc ⊢ ( 𝜑 → Fun 𝐹 )
12 funsssuppss ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
13 9 1 5 12 syl3anc ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
14 6 8 11 2 13 fsuppsssuppgd ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )