Metamath Proof Explorer

Theorem tmachlem-franscan

Description: There is a finite number of different scan sets. (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-franscan 
|- ( ph -> ran S 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 4 ffnd 
 |-  ( ph -> S Fn T )
8 fnima 
 |-  ( S Fn T -> ( S " T ) = ran S )
9 7 8 syl 
 |-  ( ph -> ( S " T ) = ran S )
10 1 2 3 4 5 6 tmachlem-exagreecover 
 |-  ( ph -> E. a ( a C_ ran A /\ a e. Fin /\ T = U. a ) )
11 simpr3 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> T = U. a )
12 11 imaeq2d 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> ( S " T ) = ( S " U. a ) )
13 imauni 
 |-  ( S " U. a ) = U_ i e. a ( S " i )
14 12 13 eqtrdi 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> ( S " T ) = U_ i e. a ( S " i ) )
15 simpr2 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> a e. Fin )
16 simpll 
 |-  ( ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) /\ i e. a ) -> ph )
17 simplr1 
 |-  ( ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) /\ i e. a ) -> a C_ ran A )
18 simpr 
 |-  ( ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) /\ i e. a ) -> i e. a )
19 17 18 sseldd 
 |-  ( ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) /\ i e. a ) -> i e. ran A )
20 1 2 3 4 5 6 tmachlem-agreefin 
 |-  ( ( ph /\ i e. ran A ) -> ( S " i ) e. Fin )
21 16 19 20 syl2anc 
 |-  ( ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) /\ i e. a ) -> ( S " i ) e. Fin )
22 21 ralrimiva 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> A. i e. a ( S " i ) e. Fin )
23 iunfi 
 |-  ( ( a e. Fin /\ A. i e. a ( S " i ) e. Fin ) -> U_ i e. a ( S " i ) e. Fin )
24 15 22 23 syl2anc 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> U_ i e. a ( S " i ) e. Fin )
25 14 24 eqeltrd 
 |-  ( ( ph /\ ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) -> ( S " T ) e. Fin )
26 10 25 exlimddv 
 |-  ( ph -> ( S " T ) e. Fin )
27 9 26 eqeltrrd 
 |-  ( ph -> ran S e. Fin )