Metamath Proof Explorer

Theorem tmachlem-uassst

Description: Union of all agreement sets only includes tapes. (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-uassst 
|- ( ph -> U. ran A C_ T )

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 5 rneqd 
 |-  ( ph -> ran A = ran ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
8 7 unieqd 
 |-  ( ph -> U. ran A = U. ran ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
9 1 2 3 4 5 6 tmachlem-extapes 
 |-  ( ph -> T e. _V )
10 9 adantr 
 |-  ( ( ph /\ z e. T ) -> T e. _V )
11 ssrab2 
 |-  { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T
12 11 a1i 
 |-  ( ( ph /\ z e. T ) -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T )
13 10 12 ssexd 
 |-  ( ( ph /\ z e. T ) -> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
14 13 ralrimiva 
 |-  ( ph -> A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V )
15 dfiun3g 
 |-  ( A. z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } e. _V -> U_ z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } = U. ran ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
16 14 15 syl 
 |-  ( ph -> U_ z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } = U. ran ( z e. T |-> { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } ) )
17 8 16 eqtr4d 
 |-  ( ph -> U. ran A = U_ z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } )
18 12 iunssd 
 |-  ( ph -> U_ z e. T { y e. T | ( y |` ( S ` z ) ) = ( z |` ( S ` z ) ) } C_ T )
19 17 18 eqsstrd 
 |-  ( ph -> U. ran A C_ T )