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 )