Metamath Proof Explorer

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 
|- ( 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-tpopen 
|- ( ( ph /\ a e. T ) -> X_ b e. I if ( b e. ( S ` a ) , { ( a ` b ) } , U ) e. ( Xt_ ` ( i e. I |-> ~P U ) ) )

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 2 adantr 
 |-  ( ( ph /\ a e. T ) -> I e. _V )
8 distop 
 |-  ( U e. Fin -> ~P U e. Top )
9 1 8 syl 
 |-  ( ph -> ~P U e. Top )
10 9 adantr 
 |-  ( ( ph /\ a e. T ) -> ~P U e. Top )
11 10 adantr 
 |-  ( ( ( ph /\ a e. T ) /\ i e. I ) -> ~P U e. Top )
12 11 fmpttd 
 |-  ( ( ph /\ a e. T ) -> ( i e. I |-> ~P U ) : I --> Top )
13 1 2 3 4 5 6 tmachlem-finscan 
 |-  ( ( ph /\ a e. T ) -> ( S ` a ) e. Fin )
14 3 eleq2d 
 |-  ( ph -> ( a e. T <-> a e. ( U ^m I ) ) )
15 14 biimpa 
 |-  ( ( ph /\ a e. T ) -> a e. ( U ^m I ) )
16 elmapi 
 |-  ( a e. ( U ^m I ) -> a : I --> U )
17 15 16 syl 
 |-  ( ( ph /\ a e. T ) -> a : I --> U )
18 17 ffvelcdmda 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> ( a ` b ) e. U )
19 snelpwi 
 |-  ( ( a ` b ) e. U -> { ( a ` b ) } e. ~P U )
20 18 19 syl 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> { ( a ` b ) } e. ~P U )
21 simpll 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> ph )
22 pwidg 
 |-  ( U e. Fin -> U e. ~P U )
23 21 1 22 3syl 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> U e. ~P U )
24 20 23 ifcld 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> if ( b e. ( S ` a ) , { ( a ` b ) } , U ) e. ~P U )
25 1 2 3 4 5 6 tmachlem-tpitem 
 |-  ( ( ph /\ b e. I ) -> ( ( i e. I |-> ~P U ) ` b ) = ~P U )
26 25 adantlr 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> ( ( i e. I |-> ~P U ) ` b ) = ~P U )
27 24 26 eleqtrrd 
 |-  ( ( ( ph /\ a e. T ) /\ b e. I ) -> if ( b e. ( S ` a ) , { ( a ` b ) } , U ) e. ( ( i e. I |-> ~P U ) ` b ) )
28 eldifn 
 |-  ( b e. ( I \ ( S ` a ) ) -> -. b e. ( S ` a ) )
29 28 adantl 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> -. b e. ( S ` a ) )
30 29 iffalsed 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> if ( b e. ( S ` a ) , { ( a ` b ) } , U ) = U )
31 simpll 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> ph )
32 eldifi 
 |-  ( b e. ( I \ ( S ` a ) ) -> b e. I )
33 32 adantl 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> b e. I )
34 31 33 25 syl2anc 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> ( ( i e. I |-> ~P U ) ` b ) = ~P U )
35 34 unieqd 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> U. ( ( i e. I |-> ~P U ) ` b ) = U. ~P U )
36 unipw 
 |-  U. ~P U = U
37 35 36 eqtrdi 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> U. ( ( i e. I |-> ~P U ) ` b ) = U )
38 30 37 eqtr4d 
 |-  ( ( ( ph /\ a e. T ) /\ b e. ( I \ ( S ` a ) ) ) -> if ( b e. ( S ` a ) , { ( a ` b ) } , U ) = U. ( ( i e. I |-> ~P U ) ` b ) )
39 7 12 13 27 38 ptopn 
 |-  ( ( ph /\ a e. T ) -> X_ b e. I if ( b e. ( S ` a ) , { ( a ` b ) } , U ) e. ( Xt_ ` ( i e. I |-> ~P U ) ) )