Theorem tmachlem-tpitem

Description: Topology lemma. (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-tpitem	|- ( ( ph /\ a e. I ) -> ( ( i e. I |-> ~P U ) ` a ) = ~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		eqid	|- ( i e. I |-> ~P U ) = ( i e. I |-> ~P U )
8		eqidd	|- ( i = a -> ~P U = ~P U )
9		simpr	|- ( ( ph /\ a e. I ) -> a e. I )
10	1	pwexd	|- ( ph -> ~P U e. _V )
11	10	adantr	|- ( ( ph /\ a e. I ) -> ~P U e. _V )
12	7 8 9 11	fvmptd3	|- ( ( ph /\ a e. I ) -> ( ( i e. I |-> ~P U ) ` a ) = ~P U )