Theorem tmachlem-tpopen2

Description: Variable-renaming lemma connecting tmachlem-agreeprod and tmachlem-tpopen . (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-tpopen2	|- ( ( ph /\ a e. T ) -> ( A ` a ) e. ( Xt_ ` ( b e. I |-> ~P U ) ) )

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-agreeprod	|- ( ( ph /\ a e. T ) -> ( A ` a ) = X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) )
8	1 2 3 4 5 6	tmachlem-tpopen	|- ( ( ph /\ a e. T ) -> X_ i e. I if ( i e. ( S ` a ) , { ( a ` i ) } , U ) e. ( Xt_ ` ( b e. I |-> ~P U ) ) )
9	7 8	eqeltrd	|- ( ( ph /\ a e. T ) -> ( A ` a ) e. ( Xt_ ` ( b e. I |-> ~P U ) ) )