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 ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
psrbagres.e ⊢ E = g ∈ ℕ 0 J | g -1 ℕ ∈ Fin
psrbagres.i ⊢ φ → I ∈ V
psrbagres.j ⊢ φ → J ⊆ I
psrbagres.f ⊢ φ → F ∈ D
Assertion psrbagres ⊢ φ → F ↾ J ∈ E

Proof

Step Hyp Ref Expression
1 psrbagres.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
2 psrbagres.e ⊢ E = g ∈ ℕ 0 J | g -1 ℕ ∈ Fin
3 psrbagres.i ⊢ φ → I ∈ V
4 psrbagres.j ⊢ φ → J ⊆ I
5 psrbagres.f ⊢ φ → F ∈ D
6 1 psrbagf ⊢ F ∈ D → F : I ⟶ ℕ 0
7 5 6 syl ⊢ φ → F : I ⟶ ℕ 0
8 7 4 fssresd ⊢ φ → F ↾ J : J ⟶ ℕ 0
9 1 psrbagfsupp ⊢ F ∈ D → finSupp 0 ⁡ F
10 5 9 syl ⊢ φ → finSupp 0 ⁡ F
11 0zd ⊢ φ → 0 ∈ ℤ
12 10 11 fsuppres ⊢ φ → finSupp 0 ⁡ F ↾ J
13 5 resexd ⊢ φ → F ↾ J ∈ V
14 fcdmnn0fsuppg ⊢ F ↾ J ∈ V ∧ F ↾ J : J ⟶ ℕ 0 → finSupp 0 ⁡ F ↾ J ↔ F ↾ J -1 ℕ ∈ Fin
15 13 8 14 syl2anc ⊢ φ → finSupp 0 ⁡ F ↾ J ↔ F ↾ J -1 ℕ ∈ Fin
16 12 15 mpbid ⊢ φ → F ↾ J -1 ℕ ∈ Fin
17 3 4 ssexd ⊢ φ → J ∈ V
18 2 psrbag ⊢ J ∈ V → F ↾ J ∈ E ↔ F ↾ J : J ⟶ ℕ 0 ∧ F ↾ J -1 ℕ ∈ Fin
19 17 18 syl ⊢ φ → F ↾ J ∈ E ↔ F ↾ J : J ⟶ ℕ 0 ∧ F ↾ J -1 ℕ ∈ Fin
20 8 16 19 mpbir2and ⊢ φ → F ↾ J ∈ E