tmachlem-tpbase

Description: The base set of product topology of tapes is the set of tapes. (Contributed by Ender Ting, 28-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-tpbase	$⊢ φ \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = T$

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		distop	$⊢ U \in Fin \to 𝒫 U \in Top$
8	1 7	syl	$⊢ φ \to 𝒫 U \in Top$
9	8	ralrimivw	$⊢ φ \to \forall i \in I 𝒫 U \in Top$
10		eqid	$⊢ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
11	10	ptunimpt	$⊢ (I \in V \land \forall i \in I 𝒫 U \in Top) \to \underset{i \in I}{⨉} ⋃ 𝒫 U = ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
12	2 9 11	syl2anc	$⊢ φ \to \underset{i \in I}{⨉} ⋃ 𝒫 U = ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
13		unipw	$⊢ ⋃ 𝒫 U = U$
14	13	a1i	$⊢ φ \to ⋃ 𝒫 U = U$
15	14	oveq1d	$⊢ φ \to {⋃ 𝒫 U}^{I} = U^{I}$
16	14 1	eqeltrd	$⊢ φ \to ⋃ 𝒫 U \in Fin$
17		ixpconstg	$⊢ (I \in V \land ⋃ 𝒫 U \in Fin) \to \underset{i \in I}{⨉} ⋃ 𝒫 U = {⋃ 𝒫 U}^{I}$
18	2 16 17	syl2anc	$⊢ φ \to \underset{i \in I}{⨉} ⋃ 𝒫 U = {⋃ 𝒫 U}^{I}$
19	15 18 3	3eqtr4d	$⊢ φ \to \underset{i \in I}{⨉} ⋃ 𝒫 U = T$
20	12 19	eqtr3d	$⊢ φ \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = T$

Metamath Proof Explorer