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 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-franscan ( 𝜑 → ran 𝑆 ∈ Fin )

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 4 ffnd ⊢ ( 𝜑 → 𝑆 Fn 𝑇 )
8 fnima ⊢ ( 𝑆 Fn 𝑇 → ( 𝑆 “ 𝑇 ) = ran 𝑆 )
9 7 8 syl ⊢ ( 𝜑 → ( 𝑆 “ 𝑇 ) = ran 𝑆 )
10 1 2 3 4 5 6 tmachlem-exagreecover ⊢ ( 𝜑 → ∃ 𝑎 ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) )
11 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → 𝑇 = ∪ 𝑎 )
12 11 imaeq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → ( 𝑆 “ 𝑇 ) = ( 𝑆 “ ∪ 𝑎 ) )
13 imauni ⊢ ( 𝑆 “ ∪ 𝑎 ) = ∪ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 )
14 12 13 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → ( 𝑆 “ 𝑇 ) = ∪ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 ) )
15 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → 𝑎 ∈ Fin )
16 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) ∧ 𝑖 ∈ 𝑎 ) → 𝜑 )
17 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) ∧ 𝑖 ∈ 𝑎 ) → 𝑎 ⊆ ran 𝐴 )
18 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) ∧ 𝑖 ∈ 𝑎 ) → 𝑖 ∈ 𝑎 )
19 17 18 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) ∧ 𝑖 ∈ 𝑎 ) → 𝑖 ∈ ran 𝐴 )
20 1 2 3 4 5 6 tmachlem-agreefin ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ran 𝐴 ) → ( 𝑆 “ 𝑖 ) ∈ Fin )
21 16 19 20 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) ∧ 𝑖 ∈ 𝑎 ) → ( 𝑆 “ 𝑖 ) ∈ Fin )
22 21 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → ∀ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 ) ∈ Fin )
23 iunfi ⊢ ( ( 𝑎 ∈ Fin ∧ ∀ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 ) ∈ Fin ) → ∪ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 ) ∈ Fin )
24 15 22 23 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → ∪ 𝑖 ∈ 𝑎 ( 𝑆 “ 𝑖 ) ∈ Fin )
25 14 24 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) → ( 𝑆 “ 𝑇 ) ∈ Fin )
26 10 25 exlimddv ⊢ ( 𝜑 → ( 𝑆 “ 𝑇 ) ∈ Fin )
27 9 26 eqeltrrd ⊢ ( 𝜑 → ran 𝑆 ∈ Fin )