Theorem esplylem

Description: Lemma for esplyfv and others. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplympl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	esplympl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	esplympl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	esplympl.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	esplylem	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		esplympl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		esplympl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
3		esplympl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		esplympl.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5		nfv	⊢ Ⅎ 𝑑 𝜑
6		indf1o	⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
7		f1of	⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
8	2 6 7	3syl	⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
9	8	ffund	⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
10		breq1	⊢ ( ℎ = ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) → ( ℎ finSupp 0 ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 ) )
11		nn0ex	⊢ ℕ0 ∈ V
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ℕ0 ∈ V )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝐼 ∈ Fin )
14		ssrab2	⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
15	14	a1i	⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
16	15	sselda	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ 𝒫 𝐼 )
17	16	elpwid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ⊆ 𝐼 )
18		indf	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
19	13 17 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
20		0nn0	⊢ 0 ∈ ℕ0
21	20	a1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 0 ∈ ℕ0 )
22		1nn0	⊢ 1 ∈ ℕ0
23	22	a1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 1 ∈ ℕ0 )
24	21 23	prssd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → { 0 , 1 } ⊆ ℕ0 )
25	19 24	fssd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ ℕ0 )
26	12 13 25	elmapdd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ ( ℕ0 ↑m 𝐼 ) )
27	19 13 21	fidmfisupp	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 )
28	10 26 27	elrabd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
29	28 1	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ 𝐷 )
30	5 9 29	funimassd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )