Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-tpbase ( 𝜑 → ∪ ( ∏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 distop ⊢ ( 𝑈 ∈ Fin → 𝒫 𝑈 ∈ Top )
8 1 7 syl ⊢ ( 𝜑 → 𝒫 𝑈 ∈ Top )
9 8 ralrimivw ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 𝒫 𝑈 ∈ Top )
10 eqid ⊢ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) )
11 10 ptunimpt ⊢ ( ( 𝐼 ∈ V ∧ ∀ 𝑖 ∈ 𝐼 𝒫 𝑈 ∈ Top ) → X 𝑖 ∈ 𝐼 ∪ 𝒫 𝑈 = ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
12 2 9 11 syl2anc ⊢ ( 𝜑 → X 𝑖 ∈ 𝐼 ∪ 𝒫 𝑈 = ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
13 unipw ⊢ ∪ 𝒫 𝑈 = 𝑈
14 13 a1i ⊢ ( 𝜑 → ∪ 𝒫 𝑈 = 𝑈 )
15 14 oveq1d ⊢ ( 𝜑 → ( ∪ 𝒫 𝑈 ↑m 𝐼 ) = ( 𝑈 ↑m 𝐼 ) )
16 14 1 eqeltrd ⊢ ( 𝜑 → ∪ 𝒫 𝑈 ∈ Fin )
17 ixpconstg ⊢ ( ( 𝐼 ∈ V ∧ ∪ 𝒫 𝑈 ∈ Fin ) → X 𝑖 ∈ 𝐼 ∪ 𝒫 𝑈 = ( ∪ 𝒫 𝑈 ↑m 𝐼 ) )
18 2 16 17 syl2anc ⊢ ( 𝜑 → X 𝑖 ∈ 𝐼 ∪ 𝒫 𝑈 = ( ∪ 𝒫 𝑈 ↑m 𝐼 ) )
19 15 18 3 3eqtr4d ⊢ ( 𝜑 → X 𝑖 ∈ 𝐼 ∪ 𝒫 𝑈 = 𝑇 )
20 12 19 eqtr3d ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = 𝑇 )