Theorem tmachlem-agreeself

Description: Any tape belongs to its own agreement set. (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-agreeself	$$⊢\left(\phi \wedge a\in T\right)\to a\in A\left(a\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		reseq1	$$⊢y=a\to {y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}$$
8		tbtru	$$⊢{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\leftrightarrow \left({y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\leftrightarrow \top \right)$$
9	7 8	sylib	$$⊢y=a\to \left({y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\leftrightarrow \top \right)$$
10		simpr	$$⊢\left(\phi \wedge a\in T\right)\to a\in T$$
11		trud	$$⊢\left(\phi \wedge a\in T\right)\to \top$$
12	9 10 11	elrabd	$$⊢\left(\phi \wedge a\in T\right)\to a\in \left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}$$
13		fveq2	$$⊢z=a\to S\left(z\right)=S\left(a\right)$$
14	13	reseq2d	$$⊢z=a\to {y\upharpoonright }_{S\left(z\right)}={y\upharpoonright }_{S\left(a\right)}$$
15		id	$$⊢z=a\to z=a$$
16	15 13	reseq12d	$$⊢z=a\to {z\upharpoonright }_{S\left(z\right)}={a\upharpoonright }_{S\left(a\right)}$$
17	14 16	eqeq12d	$$⊢z=a\to \left({y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\leftrightarrow {y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right)$$
18	17	rabbidv	$$⊢z=a\to \left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}=\left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}$$
19	5	adantr	$$⊢\left(\phi \wedge a\in T\right)\to A=\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
20	1 2 3 4 5 6	tmachlem-extapes	$$⊢\phi \to T\in \mathrm{V}$$
21		ssrab2	$$⊢\left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}\subseteq T$$
22	21	a1i	$$⊢\phi \to \left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}\subseteq T$$
23	20 22	ssexd	$$⊢\phi \to \left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}\in \mathrm{V}$$
24	23	adantr	$$⊢\left(\phi \wedge a\in T\right)\to \left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}\in \mathrm{V}$$
25	18 19 10 24	fvmptd4	$$⊢\left(\phi \wedge a\in T\right)\to A\left(a\right)=\left\{y\in T|{y\upharpoonright }_{S\left(a\right)}={a\upharpoonright }_{S\left(a\right)}\right\}$$
26	12 25	eleqtrrd	$$⊢\left(\phi \wedge a\in T\right)\to a\in A\left(a\right)$$