Theorem tmachlem-tpcomp

Description: Product (discrete) topology of tapes is compact by Tychonoff's theorem. To work for infinite index sets (such as ZZ for I which is the main interpretation), it requires Choice. (Contributed by Ender Ting, 27-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
	tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
	tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
	tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
	tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion	tmachlem-tpcomp	⊢ ( 𝜑 → ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∈ Comp )

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		discmp	⊢ ( 𝑈 ∈ Fin ↔ 𝒫 𝑈 ∈ Comp )
8	1 7	sylib	⊢ ( 𝜑 → 𝒫 𝑈 ∈ Comp )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝒫 𝑈 ∈ Comp )
10	9	fmpttd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) : 𝐼 ⟶ Comp )
11		ptcmp	⊢ ( ( 𝐼 ∈ V ∧ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) : 𝐼 ⟶ Comp ) → ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∈ Comp )
12	2 10 11	syl2anc	⊢ ( 𝜑 → ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∈ Comp )