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 
|- ( ph -> U e. Fin )
tmach.exindex 
|- ( ph -> I e. _V )
tmach.tapelist 
|- ( ph -> T = ( U ^m I ) )
tmach.scanmap 
|- ( ph -> S : T --> ( ~P I i^i Fin ) )
tmach.agreemap 
|- ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
tmach.agreement 
|- ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
Assertion tmachlem-agreeself 
|- ( ( ph /\ a e. T ) -> a e. ( A ` a ) )

Proof

Step Hyp Ref Expression
1 tmach.finalph 
 |-  ( ph -> U e. Fin )
2 tmach.exindex 
 |-  ( ph -> I e. _V )
3 tmach.tapelist 
 |-  ( ph -> T = ( U ^m I ) )
4 tmach.scanmap 
 |-  ( ph -> S : T --> ( ~P I i^i Fin ) )
5 tmach.agreemap 
 |-  ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
6 tmach.agreement 
 |-  ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
7 reseq1 
 |-  ( y = a -> ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) )
8 tbtru 
 |-  ( ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) <-> ( ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) <-> T. ) )
9 7 8 sylib 
 |-  ( y = a -> ( ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) <-> T. ) )
10 simpr 
 |-  ( ( ph /\ a e. T ) -> a e. T )
11 trud 
 |-  ( ( ph /\ a e. T ) -> T. )
12 9 10 11 elrabd 
 |-  ( ( ph /\ a e. T ) -> a e. { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
13 fveq2 
 |-  ( z = a -> ( S ` z ) = ( S ` a ) )
14 13 reseq2d 
 |-  ( z = a -> ( y |` ( S ` z ) ) = ( y |` ( S ` a ) ) )
15 id 
 |-  ( z = a -> z = a )
16 15 13 reseq12d 
 |-  ( z = a -> ( z |` ( S ` z ) ) = ( a |` ( S ` a ) ) )
17 14 16 eqeq12d 
 |-  ( z = a -> ( ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) <-> ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) ) )
18 17 rabbidv 
 |-  ( z = a -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } = { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
19 5 adantr 
 |-  ( ( ph /\ a e. T ) -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
20 1 2 3 4 5 6 tmachlem-extapes 
 |-  ( ph -> T e. _V )
21 ssrab2 
 |-  { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } C_ T
22 21 a1i 
 |-  ( ph -> { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } C_ T )
23 20 22 ssexd 
 |-  ( ph -> { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } e. _V )
24 23 adantr 
 |-  ( ( ph /\ a e. T ) -> { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } e. _V )
25 18 19 10 24 fvmptd4 
 |-  ( ( ph /\ a e. T ) -> ( A ` a ) = { y e. T | ( y |` ( S ` a ) ) = ( a |` ( S ` a ) ) } )
26 12 25 eleqtrrd 
 |-  ( ( ph /\ a e. T ) -> a e. ( A ` a ) )