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

Metamath Proof Explorer

Theorem psrbagres

Description: Restrict a bag of variables in I to a bag of variables in J C_ I . (Contributed by SN, 10-Mar-2025)

Ref Expression
Hypotheses psrbagres.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psrbagres.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
psrbagres.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrbagres.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
psrbagres.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
Assertion psrbagres ( 𝜑 → ( 𝐹 ↾ 𝐽 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 psrbagres.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 psrbagres.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
3 psrbagres.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 psrbagres.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
5 psrbagres.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
6 1 psrbagf ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
7 5 6 syl ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℕ0 )
8 7 4 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
9 1 psrbagfsupp ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 finSupp 0 )
10 5 9 syl ⊢ ( 𝜑 → 𝐹 finSupp 0 )
11 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
12 10 11 fsuppres ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐽 ) finSupp 0 )
13 5 resexd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐽 ) ∈ V )
14 fcdmnn0fsuppg ⊢ ( ( ( 𝐹 ↾ 𝐽 ) ∈ V ∧ ( 𝐹 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 ) → ( ( 𝐹 ↾ 𝐽 ) finSupp 0 ↔ ( ◡ ( 𝐹 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) )
15 13 8 14 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐽 ) finSupp 0 ↔ ( ◡ ( 𝐹 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) )
16 12 15 mpbid ⊢ ( 𝜑 → ( ◡ ( 𝐹 ↾ 𝐽 ) “ ℕ ) ∈ Fin )
17 3 4 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
18 2 psrbag ⊢ ( 𝐽 ∈ V → ( ( 𝐹 ↾ 𝐽 ) ∈ 𝐸 ↔ ( ( 𝐹 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) ) )
19 17 18 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐽 ) ∈ 𝐸 ↔ ( ( 𝐹 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 ∧ ( ◡ ( 𝐹 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) ) )
20 8 16 19 mpbir2and ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐽 ) ∈ 𝐸 )