Theorem tmachlem-fssscan

Description: Any scan set is finite. (Contributed by Ender Ting, 28-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	|- ( ph -> U e. Fin )
	tmach.exindex	|- ( ph -> I e. _V )
	tmach.tapelist	|- ( ph -> T = ( U ^m I ) )
	tmach.scanmap	|- ( ph -> S : T --> ( ~P I i^i Fin ) )
	tmach.agreemap	|- ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
	tmach.agreement	|- ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
Assertion	tmachlem-fssscan	|- ( ph -> ran S C_ Fin )

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	|- ( ph -> U e. Fin )
2		tmach.exindex	|- ( ph -> I e. _V )
3		tmach.tapelist	|- ( ph -> T = ( U ^m I ) )
4		tmach.scanmap	|- ( ph -> S : T --> ( ~P I i^i Fin ) )
5		tmach.agreemap	|- ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
6		tmach.agreement	|- ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
7	4	frnd	|- ( ph -> ran S C_ ( ~P I i^i Fin ) )
8		inss2	|- ( ~P I i^i Fin ) C_ Fin
9	7 8	sstrdi	|- ( ph -> ran S C_ Fin )