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

Metamath Proof Explorer

Theorem reprfi

Description: Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
reprfi.1 ⊢ φ → A ∈ Fin
Assertion reprfi ⊢ φ → A repr ⁡ S M ∈ Fin

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 reprfi.1 ⊢ φ → A ∈ Fin
5 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
6 fzofi ⊢ 0 ..^ S ∈ Fin
7 mapfi ⊢ A ∈ Fin ∧ 0 ..^ S ∈ Fin → A 0 ..^ S ∈ Fin
8 4 6 7 sylancl ⊢ φ → A 0 ..^ S ∈ Fin
9 rabfi ⊢ A 0 ..^ S ∈ Fin → c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ∈ Fin
10 8 9 syl ⊢ φ → c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ∈ Fin
11 5 10 eqeltrd ⊢ φ → A repr ⁡ S M ∈ Fin