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 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
tmach.exindex ⊢ ( 𝜑 → 𝐼 ∈ V )
tmach.tapelist ⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
tmach.scanmap ⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
tmach.agreemap ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
tmach.agreement ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion tmachlem-exagreecover ( 𝜑 → ∃ 𝑎 ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) )

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-extpcover ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 )
8 df-rex ⊢ ( ∃ 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ↔ ∃ 𝑎 ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) )
9 7 8 sylib ⊢ ( 𝜑 → ∃ 𝑎 ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) )
11 10 elin1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → 𝑎 ∈ 𝒫 ran 𝐴 )
12 11 elpwid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → 𝑎 ⊆ ran 𝐴 )
13 10 elin2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → 𝑎 ∈ Fin )
14 1 2 3 4 5 6 tmachlem-tpbase ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = 𝑇 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = 𝑇 )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 )
17 15 16 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → 𝑇 = ∪ 𝑎 )
18 12 13 17 3jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) ) → ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) )
19 18 ex ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) → ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) )
20 19 eximdv ⊢ ( 𝜑 → ( ∃ 𝑎 ( 𝑎 ∈ ( 𝒫 ran 𝐴 ∩ Fin ) ∧ ∪ ( ∏t ‘ ( 𝑖 ∈ 𝐼 ↦ 𝒫 𝑈 ) ) = ∪ 𝑎 ) → ∃ 𝑎 ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) ) )
21 9 20 mpd ⊢ ( 𝜑 → ∃ 𝑎 ( 𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎 ) )