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	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
	tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
	tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
	tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
	tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion	tmachlem-agreesn	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) = { ( 𝑆 ‘ 𝑎 ) } )

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	⊢ ( 𝜑 → 𝑈 ∈ Fin )
2		tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
3		tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
4		tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
5		tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
6		tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
7		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑎 ∈ 𝑇 )
8	4	ffund	⊢ ( 𝜑 → Fun 𝑆 )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → Fun 𝑆 )
10		fveq2	⊢ ( 𝑧 = 𝑎 → ( 𝐴 ‘ 𝑧 ) = ( 𝐴 ‘ 𝑎 ) )
11		fveq2	⊢ ( 𝑧 = 𝑎 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑎 ) )
12	11	eqeq2d	⊢ ( 𝑧 = 𝑎 → ( ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) ) )
13	10 12	raleqbidv	⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) ↔ ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) ) )
14	13	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) ↔ ∀ 𝑎 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) )
15	6 14	sylib	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) )
16	15	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) )
17	16	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) )
18		fvex	⊢ ( 𝑆 ‘ 𝑎 ) ∈ V
19	18	elsn2	⊢ ( ( 𝑆 ‘ 𝑦 ) ∈ { ( 𝑆 ‘ 𝑎 ) } ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑎 ) )
20	17 19	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑦 ∈ ( 𝐴 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝑦 ) ∈ { ( 𝑆 ‘ 𝑎 ) } )
21	7 9 20	funimassd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) ⊆ { ( 𝑆 ‘ 𝑎 ) } )
22	1 2 3 4 5 6	tmachlem-agreeself	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ ( 𝐴 ‘ 𝑎 ) )
23	4	fdmd	⊢ ( 𝜑 → dom 𝑆 = 𝑇 )
24	23	eleq2d	⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑆 ↔ 𝑎 ∈ 𝑇 ) )
25	24	biimpar	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ dom 𝑆 )
26		funfvima	⊢ ( ( Fun 𝑆 ∧ 𝑎 ∈ dom 𝑆 ) → ( 𝑎 ∈ ( 𝐴 ‘ 𝑎 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) ) )
27	9 25 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑎 ∈ ( 𝐴 ‘ 𝑎 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) ) )
28	22 27	mpd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) )
29	28	snssd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → { ( 𝑆 ‘ 𝑎 ) } ⊆ ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) )
30	21 29	eqssd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) = { ( 𝑆 ‘ 𝑎 ) } )