Theorem tmachlem-tpcomp

Description: Product (discrete) topology of tapes is compact by Tychonoff's theorem. To work for infinite index sets (such as ZZ for I which is the main interpretation), it requires Choice. (Contributed by Ender Ting, 27-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-tpcomp	|- ( ph -> ( Xt_ ` ( i e. I |-> ~P U ) ) e. Comp )

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		discmp	|- ( U e. Fin <-> ~P U e. Comp )
8	1 7	sylib	|- ( ph -> ~P U e. Comp )
9	8	adantr	|- ( ( ph /\ i e. I ) -> ~P U e. Comp )
10	9	fmpttd	|- ( ph -> ( i e. I |-> ~P U ) : I --> Comp )
11		ptcmp	|- ( ( I e. _V /\ ( i e. I |-> ~P U ) : I --> Comp ) -> ( Xt_ ` ( i e. I |-> ~P U ) ) e. Comp )
12	2 10 11	syl2anc	|- ( ph -> ( Xt_ ` ( i e. I |-> ~P U ) ) e. Comp )