tmachlem-tpopen

Description: Agreement sets are open in the product topology of tapes. (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-tpopen	$⊢ (φ \land a \in T) \to \underset{b \in I}{⨉} if (b \in S (a), \{a (b)\}, U) \in \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$

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	2	adantr	$⊢ (φ \land a \in T) \to I \in V$
8		distop	$⊢ U \in Fin \to 𝒫 U \in Top$
9	1 8	syl	$⊢ φ \to 𝒫 U \in Top$
10	9	adantr	$⊢ (φ \land a \in T) \to 𝒫 U \in Top$
11	10	adantr	$⊢ ((φ \land a \in T) \land i \in I) \to 𝒫 U \in Top$
12	11	fmpttd	$⊢ (φ \land a \in T) \to (i \in I ⟼ 𝒫 U) : I ⟶ Top$
13	1 2 3 4 5 6	tmachlem-finscan	$⊢ (φ \land a \in T) \to S (a) \in Fin$
14	3	eleq2d	$⊢ φ \to (a \in T \leftrightarrow a \in (U^{I}))$
15	14	biimpa	$⊢ (φ \land a \in T) \to a \in (U^{I})$
16		elmapi	$⊢ a \in (U^{I}) \to a : I ⟶ U$
17	15 16	syl	$⊢ (φ \land a \in T) \to a : I ⟶ U$
18	17	ffvelcdmda	$⊢ ((φ \land a \in T) \land b \in I) \to a (b) \in U$
19		snelpwi	$⊢ a (b) \in U \to \{a (b)\} \in 𝒫 U$
20	18 19	syl	$⊢ ((φ \land a \in T) \land b \in I) \to \{a (b)\} \in 𝒫 U$
21		simpll	$⊢ ((φ \land a \in T) \land b \in I) \to φ$
22		pwidg	$⊢ U \in Fin \to U \in 𝒫 U$
23	21 1 22	3syl	$⊢ ((φ \land a \in T) \land b \in I) \to U \in 𝒫 U$
24	20 23	ifcld	$⊢ ((φ \land a \in T) \land b \in I) \to if (b \in S (a), \{a (b)\}, U) \in 𝒫 U$
25	1 2 3 4 5 6	tmachlem-tpitem	$⊢ (φ \land b \in I) \to (i \in I ⟼ 𝒫 U) (b) = 𝒫 U$
26	25	adantlr	$⊢ ((φ \land a \in T) \land b \in I) \to (i \in I ⟼ 𝒫 U) (b) = 𝒫 U$
27	24 26	eleqtrrd	$⊢ ((φ \land a \in T) \land b \in I) \to if (b \in S (a), \{a (b)\}, U) \in (i \in I ⟼ 𝒫 U) (b)$
28		eldifn	$⊢ b \in (I ∖ S (a)) \to \neg b \in S (a)$
29	28	adantl	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to \neg b \in S (a)$
30	29	iffalsed	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to if (b \in S (a), \{a (b)\}, U) = U$
31		simpll	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to φ$
32		eldifi	$⊢ b \in (I ∖ S (a)) \to b \in I$
33	32	adantl	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to b \in I$
34	31 33 25	syl2anc	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to (i \in I ⟼ 𝒫 U) (b) = 𝒫 U$
35	34	unieqd	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to ⋃ (i \in I ⟼ 𝒫 U) (b) = ⋃ 𝒫 U$
36		unipw	$⊢ ⋃ 𝒫 U = U$
37	35 36	eqtrdi	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to ⋃ (i \in I ⟼ 𝒫 U) (b) = U$
38	30 37	eqtr4d	$⊢ ((φ \land a \in T) \land b \in (I ∖ S (a))) \to if (b \in S (a), \{a (b)\}, U) = ⋃ (i \in I ⟼ 𝒫 U) (b)$
39	7 12 13 27 38	ptopn	$⊢ (φ \land a \in T) \to \underset{b \in I}{⨉} if (b \in S (a), \{a (b)\}, U) \in \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$

Metamath Proof Explorer

Theorem tmachlem-tpopen

Proof