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 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-agreefin ( ( 𝜑 ∧ 𝑏 ∈ 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 funmpt ⊢ Fun ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } )
8 5 funeqd ⊢ ( 𝜑 → ( Fun 𝐴 ↔ Fun ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) ) )
9 7 8 mpbiri ⊢ ( 𝜑 → Fun 𝐴 )
10 elrnrexdm ⊢ ( Fun 𝐴 → ( 𝑏 ∈ ran 𝐴 → ∃ 𝑎 ∈ dom 𝐴 𝑏 = ( 𝐴 ‘ 𝑎 ) ) )
11 9 10 syl ⊢ ( 𝜑 → ( 𝑏 ∈ ran 𝐴 → ∃ 𝑎 ∈ dom 𝐴 𝑏 = ( 𝐴 ‘ 𝑎 ) ) )
12 11 imp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) → ∃ 𝑎 ∈ dom 𝐴 𝑏 = ( 𝐴 ‘ 𝑎 ) )
13 simprr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → 𝑏 = ( 𝐴 ‘ 𝑎 ) )
14 13 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → ( 𝑆 “ 𝑏 ) = ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) )
15 simpll ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → 𝜑 )
16 simprl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → 𝑎 ∈ dom 𝐴 )
17 5 dmeqd ⊢ ( 𝜑 → dom 𝐴 = dom ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
18 1 2 3 4 5 6 tmachlem-extapes ⊢ ( 𝜑 → 𝑇 ∈ V )
19 ssrab2 ⊢ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇
20 19 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇 )
21 18 20 ssexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
22 21 ralrimivw ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
23 dmmptg ⊢ ( ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V → dom ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) = 𝑇 )
24 22 23 syl ⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) = 𝑇 )
25 17 24 eqtrd ⊢ ( 𝜑 → dom 𝐴 = 𝑇 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → dom 𝐴 = 𝑇 )
27 16 26 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → 𝑎 ∈ 𝑇 )
28 1 2 3 4 5 6 tmachlem-agreesn ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) = { ( 𝑆 ‘ 𝑎 ) } )
29 15 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → ( 𝑆 “ ( 𝐴 ‘ 𝑎 ) ) = { ( 𝑆 ‘ 𝑎 ) } )
30 14 29 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → ( 𝑆 “ 𝑏 ) = { ( 𝑆 ‘ 𝑎 ) } )
31 snfi ⊢ { ( 𝑆 ‘ 𝑎 ) } ∈ Fin
32 30 31 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) ∧ ( 𝑎 ∈ dom 𝐴 ∧ 𝑏 = ( 𝐴 ‘ 𝑎 ) ) ) → ( 𝑆 “ 𝑏 ) ∈ Fin )
33 12 32 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐴 ) → ( 𝑆 “ 𝑏 ) ∈ Fin )