Metamath Proof Explorer

Theorem tmachlem-exagreecover

Description: Particular properties of the finite cover of agreesets. (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-exagreecover 
|- ( ph -> E. a ( a C_ ran A /\ a e. Fin /\ T = 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-extpcover 
 |-  ( ph -> E. a e. ( ~P ran A i^i Fin ) U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a )
8 df-rex 
 |-  ( E. a e. ( ~P ran A i^i Fin ) U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a <-> E. a ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) )
9 7 8 sylib 
 |-  ( ph -> E. a ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) )
10 simprl 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> a e. ( ~P ran A i^i Fin ) )
11 10 elin1d 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> a e. ~P ran A )
12 11 elpwid 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> a C_ ran A )
13 10 elin2d 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> a e. Fin )
14 1 2 3 4 5 6 tmachlem-tpbase 
 |-  ( ph -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = T )
15 14 adantr 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = T )
16 simprr 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a )
17 15 16 eqtr3d 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> T = U. a )
18 12 13 17 3jca 
 |-  ( ( ph /\ ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) ) -> ( a C_ ran A /\ a e. Fin /\ T = U. a ) )
19 18 ex 
 |-  ( ph -> ( ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) -> ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) )
20 19 eximdv 
 |-  ( ph -> ( E. a ( a e. ( ~P ran A i^i Fin ) /\ U. ( Xt_ ` ( i e. I |-> ~P U ) ) = U. a ) -> E. a ( a C_ ran A /\ a e. Fin /\ T = U. a ) ) )
21 9 20 mpd 
 |-  ( ph -> E. a ( a C_ ran A /\ a e. Fin /\ T = U. a ) )