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 
|- ( ph -> U e. Fin )
tmach.exindex 
|- ( ph -> I e. _V )
tmach.tapelist 
|- ( ph -> T = ( U ^m I ) )
tmach.scanmap 
|- ( ph -> S : T --> ( ~P I i^i Fin ) )
tmach.agreemap 
|- ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
tmach.agreement 
|- ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
Assertion tmachlem-extpcover 
|- ( ph -> E. a e. ( ~P ran A i^i Fin ) U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a )

Proof

Step Hyp Ref Expression
1 tmach.finalph 
 |-  ( ph -> U e. Fin )
2 tmach.exindex 
 |-  ( ph -> I e. _V )
3 tmach.tapelist 
 |-  ( ph -> T = ( U ^m I ) )
4 tmach.scanmap 
 |-  ( ph -> S : T --> ( ~P I i^i Fin ) )
5 tmach.agreemap 
 |-  ( ph -> A = ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
6 tmach.agreement 
 |-  ( ph -> A. z e. T A. y e. ( A ` z ) ( S ` y ) = ( S ` z ) )
7 1 2 3 4 5 6 tmachlem-tpcomp 
 |-  ( ph -> ( Xt_ ` ( i e. I |-> ~P U ) ) e. Comp )
8 1 2 3 4 5 6 tmachlem-extapes 
 |-  ( ph -> T e. _V )
9 ssrab2 
 |-  { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T
10 9 a1i 
 |-  ( ph -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T )
11 8 10 ssexd 
 |-  ( ph -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
12 11 ralrimivw 
 |-  ( ph -> A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
13 nfcv 
 |-  F/_ z T
14 13 mptfnf 
 |-  ( A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V <-> ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) Fn T )
15 12 14 sylib 
 |-  ( ph -> ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) Fn T )
16 5 fneq1d 
 |-  ( ph -> ( A Fn T <-> ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) Fn T ) )
17 15 16 mpbird 
 |-  ( ph -> A Fn T )
18 1 2 3 4 5 6 tmachlem-tpopen2 
 |-  ( ( ph /\ b e. T ) -> ( A ` b ) e. ( Xt_ ` ( i e. I |-> ~P U ) ) )
19 18 ralrimiva 
 |-  ( ph -> A. b e. T ( A ` b ) e. ( Xt_ ` ( i e. I |-> ~P U ) ) )
20 fnfvrnss 
 |-  ( ( A Fn T /\ A. b e. T ( A ` b ) e. ( Xt_ ` ( i e. I |-> ~P U ) ) ) -> ran A C_ ( Xt_ ` ( i e. I |-> ~P U ) ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ran A C_ ( Xt_ ` ( i e. I |-> ~P U ) ) )
22 1 2 3 4 5 6 tmachlem-tpbase 
 |-  ( ph -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = T )
23 1 2 3 4 5 6 tmachlem-exlargecover 
 |-  ( ph -> U. ran A = T )
24 22 23 eqtr4d 
 |-  ( ph -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. ran A )
25 eqid 
 |-  U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. ( Xt_ ` ( i e. I |-> ~P U ) )
26 25 cmpcov 
 |-  ( ( ( Xt_ ` ( i e. I |-> ~P U ) ) e. Comp /\ ran A C_ ( Xt_ ` ( i e. I |-> ~P U ) ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. ran A ) -> E. a e. ( ~P ran A i^i Fin ) U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a )
27 7 21 24 26 syl3anc 
 |-  ( ph -> E. a e. ( ~P ran A i^i Fin ) U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a )