Theorem tmachlem-exlargecover

Description: Product topology of tapes has an open cover. (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-exlargecover	|- ( ph -> U. ran A = T )

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	1 2 3 4 5 6	tmachlem-uassst	|- ( ph -> U. ran A C_ T )
8	1 2 3 4 5 6	tmachlem-agreeself	|- ( ( ph /\ a e. T ) -> a e. ( A ` a ) )
9		elfvunirn	|- ( a e. ( A ` a ) -> a e. U. ran A )
10	8 9	syl	|- ( ( ph /\ a e. T ) -> a e. U. ran A )
11	7 10	eqelssd	|- ( ph -> U. ran A = T )