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 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprfi.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion reprfi ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 reprfi.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 1 2 3 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
6 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
7 mapfi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 0 ..^ 𝑆 ) ∈ Fin ) → ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∈ Fin )
8 4 6 7 sylancl ⊢ ( 𝜑 → ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∈ Fin )
9 rabfi ⊢ ( ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∈ Fin → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ Fin )
10 8 9 syl ⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ Fin )
11 5 10 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) ∈ Fin )