Metamath Proof Explorer

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	$⊢ φ \to U \in Fin$
		tmach.exindex	$⊢ φ \to I \in V$
		tmach.tapelist	$⊢ φ \to T = U^{I}$
		tmach.scanmap	$⊢ φ \to S : T ⟶ 𝒫 I \cap Fin$
		tmach.agreemap	$⊢ φ \to A = (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
		tmach.agreement	$⊢ φ \to \forall z \in T \forall y \in A (z) S (y) = S (z)$
	Assertion	tmachlem-tpcomp	$⊢ φ \to \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \in Comp$

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	$⊢ φ \to U \in Fin$
2		tmach.exindex	$⊢ φ \to I \in V$
3		tmach.tapelist	$⊢ φ \to T = U^{I}$
4		tmach.scanmap	$⊢ φ \to S : T ⟶ 𝒫 I \cap Fin$
5		tmach.agreemap	$⊢ φ \to A = (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
6		tmach.agreement	$⊢ φ \to \forall z \in T \forall y \in A (z) S (y) = S (z)$
7		discmp	$⊢ U \in Fin \leftrightarrow 𝒫 U \in Comp$
8	1 7	sylib	$⊢ φ \to 𝒫 U \in Comp$
9	8	adantr	$⊢ (φ \land i \in I) \to 𝒫 U \in Comp$
10	9	fmpttd	$⊢ φ \to (i \in I ⟼ 𝒫 U) : I ⟶ Comp$
11		ptcmp	$⊢ (I \in V \land (i \in I ⟼ 𝒫 U) : I ⟶ Comp) \to \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \in Comp$
12	2 10 11	syl2anc	$⊢ φ \to \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \in Comp$