Theorem tmachlem-agreesn

Description: Scans for all tapes of a single agreement set are identical. (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-agreesn	$$⊢\left(\phi \wedge a\in T\right)\to S\left[A\left(a\right)\right]=\left\{S\left(a\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		nfv	$$⊢Ⅎy\left(\phi \wedge a\in T\right)$$
8	4	ffund	$$⊢\phi \to \mathrm{Fun}S$$
9	8	adantr	$$⊢\left(\phi \wedge a\in T\right)\to \mathrm{Fun}S$$
10		fveq2	$$⊢z=a\to A\left(z\right)=A\left(a\right)$$
11		fveq2	$$⊢z=a\to S\left(z\right)=S\left(a\right)$$
12	11	eqeq2d	$$⊢z=a\to \left(S\left(y\right)=S\left(z\right)\leftrightarrow S\left(y\right)=S\left(a\right)\right)$$
13	10 12	raleqbidv	$$⊢z=a\to \left(\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)\leftrightarrow \forall y\in A\left(a\right)S\left(y\right)=S\left(a\right)\right)$$
14	13	cbvralvw	$$⊢\forall z\in T\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)\leftrightarrow \forall a\in T\forall y\in A\left(a\right)S\left(y\right)=S\left(a\right)$$
15	6 14	sylib	$$⊢\phi \to \forall a\in T\forall y\in A\left(a\right)S\left(y\right)=S\left(a\right)$$
16	15	r19.21bi	$$⊢\left(\phi \wedge a\in T\right)\to \forall y\in A\left(a\right)S\left(y\right)=S\left(a\right)$$
17	16	r19.21bi	$$⊢\left(\left(\phi \wedge a\in T\right)\wedge y\in A\left(a\right)\right)\to S\left(y\right)=S\left(a\right)$$
18		fvex	$$⊢S\left(a\right)\in \mathrm{V}$$
19	18	elsn2	$$⊢S\left(y\right)\in \left\{S\left(a\right)\right\}\leftrightarrow S\left(y\right)=S\left(a\right)$$
20	17 19	sylibr	$$⊢\left(\left(\phi \wedge a\in T\right)\wedge y\in A\left(a\right)\right)\to S\left(y\right)\in \left\{S\left(a\right)\right\}$$
21	7 9 20	funimassd	$$⊢\left(\phi \wedge a\in T\right)\to S\left[A\left(a\right)\right]\subseteq \left\{S\left(a\right)\right\}$$
22	1 2 3 4 5 6	tmachlem-agreeself	$$⊢\left(\phi \wedge a\in T\right)\to a\in A\left(a\right)$$
23	4	fdmd	$$⊢\phi \to \mathrm{dom}S=T$$
24	23	eleq2d	$$⊢\phi \to \left(a\in \mathrm{dom}S\leftrightarrow a\in T\right)$$
25	24	biimpar	$$⊢\left(\phi \wedge a\in T\right)\to a\in \mathrm{dom}S$$
26		funfvima	$$⊢\left(\mathrm{Fun}S\wedge a\in \mathrm{dom}S\right)\to \left(a\in A\left(a\right)\to S\left(a\right)\in S\left[A\left(a\right)\right]\right)$$
27	9 25 26	syl2anc	$$⊢\left(\phi \wedge a\in T\right)\to \left(a\in A\left(a\right)\to S\left(a\right)\in S\left[A\left(a\right)\right]\right)$$
28	22 27	mpd	$$⊢\left(\phi \wedge a\in T\right)\to S\left(a\right)\in S\left[A\left(a\right)\right]$$
29	28	snssd	$$⊢\left(\phi \wedge a\in T\right)\to \left\{S\left(a\right)\right\}\subseteq S\left[A\left(a\right)\right]$$
30	21 29	eqssd	$$⊢\left(\phi \wedge a\in T\right)\to S\left[A\left(a\right)\right]=\left\{S\left(a\right)\right\}$$