Metamath Proof Explorer

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 
|- ( 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-agreesn 
|- ( ( ph /\ a e. T ) -> ( S " ( A ` a ) ) = { ( S ` 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 nfv 
 |-  F/ y ( ph /\ a e. T )
8 4 ffund 
 |-  ( ph -> Fun S )
9 8 adantr 
 |-  ( ( ph /\ a e. T ) -> Fun S )
10 fveq2 
 |-  ( z = a -> ( A ` z ) = ( A ` a ) )
11 fveq2 
 |-  ( z = a -> ( S ` z ) = ( S ` a ) )
12 11 eqeq2d 
 |-  ( z = a -> ( ( S ` y ) = ( S ` z ) <-> ( S ` y ) = ( S ` a ) ) )
13 10 12 raleqbidv 
 |-  ( z = a -> ( A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) <-> A. y e. ( A ` a ) ( S ` y ) = ( S ` a ) ) )
14 13 cbvralvw 
 |-  ( A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) <-> A. a e. T A. y e. ( A ` a ) ( S ` y ) = ( S ` a ) )
15 6 14 sylib 
 |-  ( ph -> A. a e. T A. y e. ( A ` a ) ( S ` y ) = ( S ` a ) )
16 15 r19.21bi 
 |-  ( ( ph /\ a e. T ) -> A. y e. ( A ` a ) ( S ` y ) = ( S ` a ) )
17 16 r19.21bi 
 |-  ( ( ( ph /\ a e. T ) /\ y e. ( A ` a ) ) -> ( S ` y ) = ( S ` a ) )
18 fvex 
 |-  ( S ` a ) e. _V
19 18 elsn2 
 |-  ( ( S ` y ) e. { ( S ` a ) } <-> ( S ` y ) = ( S ` a ) )
20 17 19 sylibr 
 |-  ( ( ( ph /\ a e. T ) /\ y e. ( A ` a ) ) -> ( S ` y ) e. { ( S ` a ) } )
21 7 9 20 funimassd 
 |-  ( ( ph /\ a e. T ) -> ( S " ( A ` a ) ) C_ { ( S ` a ) } )
22 1 2 3 4 5 6 tmachlem-agreeself 
 |-  ( ( ph /\ a e. T ) -> a e. ( A ` a ) )
23 4 fdmd 
 |-  ( ph -> dom S = T )
24 23 eleq2d 
 |-  ( ph -> ( a e. dom S <-> a e. T ) )
25 24 biimpar 
 |-  ( ( ph /\ a e. T ) -> a e. dom S )
26 funfvima 
 |-  ( ( Fun S /\ a e. dom S ) -> ( a e. ( A ` a ) -> ( S ` a ) e. ( S " ( A ` a ) ) ) )
27 9 25 26 syl2anc 
 |-  ( ( ph /\ a e. T ) -> ( a e. ( A ` a ) -> ( S ` a ) e. ( S " ( A ` a ) ) ) )
28 22 27 mpd 
 |-  ( ( ph /\ a e. T ) -> ( S ` a ) e. ( S " ( A ` a ) ) )
29 28 snssd 
 |-  ( ( ph /\ a e. T ) -> { ( S ` a ) } C_ ( S " ( A ` a ) ) )
30 21 29 eqssd 
 |-  ( ( ph /\ a e. T ) -> ( S " ( A ` a ) ) = { ( S ` a ) } )