Theorem 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	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
	tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
	tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
	tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
	tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion	tmachlem-tpopen	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑏 ∈ 𝐼 if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) ∈ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )

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	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝐼 ∈ V )
8		distop	⊢ ( 𝑈 ∈ Fin → 𝒫 𝑈 ∈ Top )
9	1 8	syl	⊢ ( 𝜑 → 𝒫 𝑈 ∈ Top )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝒫 𝑈 ∈ Top )
11	10	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑖 ∈ 𝐼 ) → 𝒫 𝑈 ∈ Top )
12	11	fmpttd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) : 𝐼 ⟶ Top )
13	1 2 3 4 5 6	tmachlem-finscan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑎 ) ∈ Fin )
14	3	eleq2d	⊢ ( 𝜑 → ( 𝑎 ∈ 𝑇 ↔ 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) ) )
15	14	biimpa	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) )
16		elmapi	⊢ ( 𝑎 ∈ ( 𝑈 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝑈 )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → 𝑎 : 𝐼 ⟶ 𝑈 )
18	17	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑏 ) ∈ 𝑈 )
19		snelpwi	⊢ ( ( 𝑎 ‘ 𝑏 ) ∈ 𝑈 → { ( 𝑎 ‘ 𝑏 ) } ∈ 𝒫 𝑈 )
20	18 19	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → { ( 𝑎 ‘ 𝑏 ) } ∈ 𝒫 𝑈 )
21		simpll	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → 𝜑 )
22		pwidg	⊢ ( 𝑈 ∈ Fin → 𝑈 ∈ 𝒫 𝑈 )
23	21 1 22	3syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑈 ∈ 𝒫 𝑈 )
24	20 23	ifcld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) ∈ 𝒫 𝑈 )
25	1 2 3 4 5 6	tmachlem-tpitem	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) = 𝒫 𝑈 )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) = 𝒫 𝑈 )
27	24 26	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ 𝐼 ) → if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) ∈ ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) )
28		eldifn	⊢ ( 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) → ¬ 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) )
29	28	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → ¬ 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) )
30	29	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) = 𝑈 )
31		simpll	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → 𝜑 )
32		eldifi	⊢ ( 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) → 𝑏 ∈ 𝐼 )
33	32	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → 𝑏 ∈ 𝐼 )
34	31 33 25	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) = 𝒫 𝑈 )
35	34	unieqd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → ∪ ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) = ∪ 𝒫 𝑈 )
36		unipw	⊢ ∪ 𝒫 𝑈 = 𝑈
37	35 36	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → ∪ ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) = 𝑈 )
38	30 37	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) ∧ 𝑏 ∈ ( 𝐼 ∖ ( 𝑆 ‘ 𝑎 ) ) ) → if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) = ∪ ( ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ‘ 𝑏 ) )
39	7 12 13 27 38	ptopn	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑇 ) → X 𝑏 ∈ 𝐼 if ( 𝑏 ∈ ( 𝑆 ‘ 𝑎 ) , { ( 𝑎 ‘ 𝑏 ) } , 𝑈 ) ∈ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )