Theorem tmachlem-tpitem

Description: Topology lemma. (Contributed by Ender Ting, 27-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	$$⊢\phi \to U\in \mathrm{Fin}$$
	tmach.exindex	$$⊢\phi \to I\in \mathrm{V}$$
	tmach.tapelist	$$⊢\phi \to T=U^I$$
	tmach.scanmap	$$⊢\phi \to S:T⟶𝒫I\cap \mathrm{Fin}$$
	tmach.agreemap	$$⊢\phi \to A=\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
	tmach.agreement	$$⊢\phi \to \forall z\in T\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)$$
Assertion	tmachlem-tpitem	$$⊢\left(\phi \wedge a\in I\right)\to \left(i\in I⟼𝒫U\right)\left(a\right)=𝒫U$$

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	$$⊢\phi \to U\in \mathrm{Fin}$$
2		tmach.exindex	$$⊢\phi \to I\in \mathrm{V}$$
3		tmach.tapelist	$$⊢\phi \to T=U^I$$
4		tmach.scanmap	$$⊢\phi \to S:T⟶𝒫I\cap \mathrm{Fin}$$
5		tmach.agreemap	$$⊢\phi \to A=\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
6		tmach.agreement	$$⊢\phi \to \forall z\in T\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)$$
7		eqid	$$⊢\left(i\in I⟼𝒫U\right)=\left(i\in I⟼𝒫U\right)$$
8		eqidd	$$⊢i=a\to 𝒫U=𝒫U$$
9		simpr	$$⊢\left(\phi \wedge a\in I\right)\to a\in I$$
10	1	pwexd	$$⊢\phi \to 𝒫U\in \mathrm{V}$$
11	10	adantr	$$⊢\left(\phi \wedge a\in I\right)\to 𝒫U\in \mathrm{V}$$
12	7 8 9 11	fvmptd3	$$⊢\left(\phi \wedge a\in I\right)\to \left(i\in I⟼𝒫U\right)\left(a\right)=𝒫U$$