Theorem tmachlem-uassst

Description: Union of all agreement sets only includes tapes. (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-uassst	$$⊢\phi \to \bigcup \mathrm{ran}A\subseteq 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	5	rneqd	$$⊢\phi \to \mathrm{ran}A=\mathrm{ran}\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
8	7	unieqd	$$⊢\phi \to \bigcup \mathrm{ran}A=\bigcup \mathrm{ran}\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
9	1 2 3 4 5 6	tmachlem-extapes	$$⊢\phi \to T\in \mathrm{V}$$
10	9	adantr	$$⊢\left(\phi \wedge z\in T\right)\to T\in \mathrm{V}$$
11		ssrab2	$$⊢\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\subseteq T$$
12	11	a1i	$$⊢\left(\phi \wedge z\in T\right)\to \left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\subseteq T$$
13	10 12	ssexd	$$⊢\left(\phi \wedge z\in T\right)\to \left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\in \mathrm{V}$$
14	13	ralrimiva	$$⊢\phi \to \forall z\in T\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\in \mathrm{V}$$
15		dfiun3g	$$⊢\forall z\in T\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\in \mathrm{V}\to \bigcup _{z\in T}\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}=\bigcup \mathrm{ran}\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
16	14 15	syl	$$⊢\phi \to \bigcup _{z\in T}\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}=\bigcup \mathrm{ran}\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
17	8 16	eqtr4d	$$⊢\phi \to \bigcup \mathrm{ran}A=\bigcup _{z\in T}\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}$$
18	12	iunssd	$$⊢\phi \to \bigcup _{z\in T}\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\subseteq T$$
19	17 18	eqsstrd	$$⊢\phi \to \bigcup \mathrm{ran}A\subseteq T$$