Metamath Proof Explorer

Theorem esplylem

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

Ref Expression
Hypotheses esplympl.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
esplympl.i ⊢ φ → I ∈ Fin
esplympl.r ⊢ φ → R ∈ Ring
esplympl.k ⊢ φ → K ∈ ℕ 0
Assertion esplylem ⊢ φ → 𝟙 I c ∈ 𝒫 I | c = K ⊆ D

Proof

Step Hyp Ref Expression
1 esplympl.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 esplympl.i ⊢ φ → I ∈ Fin
3 esplympl.r ⊢ φ → R ∈ Ring
4 esplympl.k ⊢ φ → K ∈ ℕ 0
5 nfv ⊢ Ⅎ d φ
6 indf1o ⊢ I ∈ Fin → 𝟙 I : 𝒫 I ⟶ 1-1 onto 0 1 I
7 f1of ⊢ 𝟙 I : 𝒫 I ⟶ 1-1 onto 0 1 I → 𝟙 I : 𝒫 I ⟶ 0 1 I
8 2 6 7 3syl ⊢ φ → 𝟙 I : 𝒫 I ⟶ 0 1 I
9 8 ffund ⊢ φ → Fun ⁡ 𝟙 I
10 breq1 ⊢ h = 𝟙 I ⁡ d → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ 𝟙 I ⁡ d
11 nn0ex ⊢ ℕ 0 ∈ V
12 11 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → ℕ 0 ∈ V
13 2 adantr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → I ∈ Fin
14 ssrab2 ⊢ c ∈ 𝒫 I | c = K ⊆ 𝒫 I
15 14 a1i ⊢ φ → c ∈ 𝒫 I | c = K ⊆ 𝒫 I
16 15 sselda ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d ∈ 𝒫 I
17 16 elpwid ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d ⊆ I
18 indf ⊢ I ∈ Fin ∧ d ⊆ I → 𝟙 I ⁡ d : I ⟶ 0 1
19 13 17 18 syl2anc ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d : I ⟶ 0 1
20 0nn0 ⊢ 0 ∈ ℕ 0
21 20 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 0 ∈ ℕ 0
22 1nn0 ⊢ 1 ∈ ℕ 0
23 22 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 1 ∈ ℕ 0
24 21 23 prssd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 0 1 ⊆ ℕ 0
25 19 24 fssd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d : I ⟶ ℕ 0
26 12 13 25 elmapdd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ ℕ 0 I
27 19 13 21 fidmfisupp ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → finSupp 0 ⁡ 𝟙 I ⁡ d
28 10 26 27 elrabd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h
29 28 1 eleqtrrdi ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ D
30 5 9 29 funimassd ⊢ φ → 𝟙 I c ∈ 𝒫 I | c = K ⊆ D