Metamath Proof Explorer

Theorem tmachlem-agreefin

Description: Any agreement set has a finite (singleton) list of possible scans. (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-agreefin 
|- ( ( ph /\ b e. ran A ) -> ( S " b ) e. Fin )

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 funmpt 
 |-  Fun ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } )
8 5 funeqd 
 |-  ( ph -> ( Fun A <-> Fun ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) ) )
9 7 8 mpbiri 
 |-  ( ph -> Fun A )
10 elrnrexdm 
 |-  ( Fun A -> ( b e. ran A -> E. a e. dom A b = ( A ` a ) ) )
11 9 10 syl 
 |-  ( ph -> ( b e. ran A -> E. a e. dom A b = ( A ` a ) ) )
12 11 imp 
 |-  ( ( ph /\ b e. ran A ) -> E. a e. dom A b = ( A ` a ) )
13 simprr 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> b = ( A ` a ) )
14 13 imaeq2d 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> ( S " b ) = ( S " ( A ` a ) ) )
15 simpll 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> ph )
16 simprl 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> a e. dom A )
17 5 dmeqd 
 |-  ( ph -> dom A = dom ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
18 1 2 3 4 5 6 tmachlem-extapes 
 |-  ( ph -> T e. _V )
19 ssrab2 
 |-  { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T
20 19 a1i 
 |-  ( ph -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T )
21 18 20 ssexd 
 |-  ( ph -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
22 21 ralrimivw 
 |-  ( ph -> A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
23 dmmptg 
 |-  ( A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V -> dom ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) = T )
24 22 23 syl 
 |-  ( ph -> dom ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) = T )
25 17 24 eqtrd 
 |-  ( ph -> dom A = T )
26 25 ad2antrr 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> dom A = T )
27 16 26 eleqtrd 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> a e. T )
28 1 2 3 4 5 6 tmachlem-agreesn 
 |-  ( ( ph /\ a e. T ) -> ( S " ( A ` a ) ) = { ( S ` a ) } )
29 15 27 28 syl2anc 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> ( S " ( A ` a ) ) = { ( S ` a ) } )
30 14 29 eqtrd 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> ( S " b ) = { ( S ` a ) } )
31 snfi 
 |-  { ( S ` a ) } e. Fin
32 30 31 eqeltrdi 
 |-  ( ( ( ph /\ b e. ran A ) /\ ( a e. dom A /\ b = ( A ` a ) ) ) -> ( S " b ) e. Fin )
33 12 32 rexlimddv 
 |-  ( ( ph /\ b e. ran A ) -> ( S " b ) e. Fin )