Metamath Proof Explorer

Theorem tmachlem-extpcover

Description: Product topology of tapes admits finite cover. (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-extpcover ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∪ ( ∏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 1 2 3 4 5 6 tmachlem-tpcomp ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∈ Comp )
8 1 2 3 4 5 6 tmachlem-extapes ⊢ ( 𝜑 → 𝑇 ∈ V )
9 ssrab2 ⊢ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇
10 9 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ⊆ 𝑇 )
11 8 10 ssexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
12 11 ralrimivw ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V )
13 nfcv ⊢ Ⅎ 𝑧 𝑇
14 13 mptfnf ⊢ ( ∀ 𝑧 ∈ 𝑇 { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ∈ V ↔ ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) Fn 𝑇 )
15 12 14 sylib ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) Fn 𝑇 )
16 5 fneq1d ⊢ ( 𝜑 → ( 𝐴 Fn 𝑇 ↔ ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) Fn 𝑇 ) )
17 15 16 mpbird ⊢ ( 𝜑 → 𝐴 Fn 𝑇 )
18 1 2 3 4 5 6 tmachlem-tpopen2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑏 ) ∈ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
19 18 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝑇 ( 𝐴 ‘ 𝑏 ) ∈ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
20 fnfvrnss ⊢ ( ( 𝐴 Fn 𝑇 ∧ ∀ 𝑏 ∈ 𝑇 ( 𝐴 ‘ 𝑏 ) ∈ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ) → ran 𝐴 ⊆ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ran 𝐴 ⊆ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) )
22 1 2 3 4 5 6 tmachlem-tpbase ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = 𝑇 )
23 1 2 3 4 5 6 tmachlem-exlargecover ⊢ ( 𝜑 → ∪ ran 𝐴 = 𝑇 )
24 22 23 eqtr4d ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ ran 𝐴 )
25 eqid ⊢ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) )
26 25 cmpcov ⊢ ( ( ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∈ Comp ∧ ran 𝐴 ⊆ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ ran 𝐴 ) → ∃ 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 )
27 7 21 24 26 syl3anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 )