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	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐽 ) ∈ 𝐸 )