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	$$⊢\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-tpopen2	$$⊢\left(\phi \wedge a\in T\right)\to A\left(a\right)\in {\prod }_{𝑡}\left(\left(b\in I⟼𝒫U\right)\right)$$

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	1 2 3 4 5 6	tmachlem-agreeprod	$$⊢\left(\phi \wedge a\in T\right)\to A\left(a\right)=\underset{i\in I}{⨉}if\left(i\in S\left(a\right),\left\{a\left(i\right)\right\},U\right)$$
8	1 2 3 4 5 6	tmachlem-tpopen	$$⊢\left(\phi \wedge a\in T\right)\to \underset{i\in I}{⨉}if\left(i\in S\left(a\right),\left\{a\left(i\right)\right\},U\right)\in {\prod }_{𝑡}\left(\left(b\in I⟼𝒫U\right)\right)$$
9	7 8	eqeltrd	$$⊢\left(\phi \wedge a\in T\right)\to A\left(a\right)\in {\prod }_{𝑡}\left(\left(b\in I⟼𝒫U\right)\right)$$