Theorem tmachlem-tpbase

Description: The base set of product topology of tapes is the set of tapes. (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-tpbase	|- ( ph -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = 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		distop	|- ( U e. Fin -> ~P U e. Top )
8	1 7	syl	|- ( ph -> ~P U e. Top )
9	8	ralrimivw	|- ( ph -> A. i e. I ~P U e. Top )
10		eqid	|- ( Xt_ ` ( i e. I |-> ~P U ) ) = ( Xt_ ` ( i e. I |-> ~P U ) )
11	10	ptunimpt	|- ( ( I e. _V /\ A. i e. I ~P U e. Top ) -> X_ i e. I U. ~P U = U. ( Xt_ ` ( i e. I |-> ~P U ) ) )
12	2 9 11	syl2anc	|- ( ph -> X_ i e. I U. ~P U = U. ( Xt_ ` ( i e. I |-> ~P U ) ) )
13		unipw	|- U. ~P U = U
14	13	a1i	|- ( ph -> U. ~P U = U )
15	14	oveq1d	|- ( ph -> ( U. ~P U ^m I ) = ( U ^m I ) )
16	14 1	eqeltrd	|- ( ph -> U. ~P U e. Fin )
17		ixpconstg	|- ( ( I e. _V /\ U. ~P U e. Fin ) -> X_ i e. I U. ~P U = ( U. ~P U ^m I ) )
18	2 16 17	syl2anc	|- ( ph -> X_ i e. I U. ~P U = ( U. ~P U ^m I ) )
19	15 18 3	3eqtr4d	|- ( ph -> X_ i e. I U. ~P U = T )
20	12 19	eqtr3d	|- ( ph -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = T )