Theorem tmachlem-exlargecover

Description: Product topology of tapes has an open cover. (Contributed by Ender Ting, 28-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-exlargecover	$$⊢\phi \to \bigcup \mathrm{ran}A=T$$

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-uassst	$$⊢\phi \to \bigcup \mathrm{ran}A\subseteq T$$
8	1 2 3 4 5 6	tmachlem-agreeself	$$⊢\left(\phi \wedge a\in T\right)\to a\in A\left(a\right)$$
9		elfvunirn	$$⊢a\in A\left(a\right)\to a\in \bigcup \mathrm{ran}A$$
10	8 9	syl	$$⊢\left(\phi \wedge a\in T\right)\to a\in \bigcup \mathrm{ran}A$$
11	7 10	eqelssd	$$⊢\phi \to \bigcup \mathrm{ran}A=T$$