Metamath Proof Explorer

Theorem tmachlem-agreeself

Description: Any tape belongs to its own agreement set. (Contributed by Ender Ting, 27-Jul-2026)

Ref Expression
Hypotheses tmach.finalph ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-agreeself ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ ( 𝐴 ‘ 𝑎 ) )

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 reseq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) )
8 tbtru ⊢ ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ↔ ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ↔ ⊤ ) )
9 7 8 sylib ⊢ ( 𝑦 = 𝑎 → ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ↔ ⊤ ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ 𝑇 )
11 trud ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ⊤ )
12 9 10 11 elrabd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
13 fveq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑎 ) )
14 13 reseq2d ⊢ ( 𝑧 = 𝑎 → ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) )
15 id ⊢ ( 𝑧 = 𝑎 → 𝑧 = 𝑎 )
16 15 13 reseq12d ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) ↔ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) ) )
18 17 rabbidv ⊢ ( 𝑧 = 𝑎 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } = { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
20 1 2 3 4 5 6 tmachlem-extapes ⊢ ( 𝜑 → 𝑇 ∈ V )
21 ssrab2 ⊢ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ⊆ 𝑇
22 21 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ⊆ 𝑇 )
23 20 22 ssexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ∈ V )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } ∈ V )
25 18 19 10 24 fvmptd4 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑎 ) = { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑎 ) ) = ( 𝑎 ↾ ( 𝑆 ‘ 𝑎 ) ) } )
26 12 25 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ ( 𝐴 ‘ 𝑎 ) )