tmachlem-exagreecover

Description: Particular properties of the finite cover of agreesets. (Contributed by Ender Ting, 28-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	$⊢ φ \to U \in Fin$
	tmach.exindex	$⊢ φ \to I \in V$
	tmach.tapelist	$⊢ φ \to T = U^{I}$
	tmach.scanmap	$⊢ φ \to S : T ⟶ 𝒫 I \cap Fin$
	tmach.agreemap	$⊢ φ \to A = (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
	tmach.agreement	$⊢ φ \to \forall z \in T \forall y \in A (z) S (y) = S (z)$
Assertion	tmachlem-exagreecover	$⊢ φ \to \exists a (a \subseteq ran A \land a \in Fin \land T = ⋃ a)$

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	$⊢ φ \to U \in Fin$
2		tmach.exindex	$⊢ φ \to I \in V$
3		tmach.tapelist	$⊢ φ \to T = U^{I}$
4		tmach.scanmap	$⊢ φ \to S : T ⟶ 𝒫 I \cap Fin$
5		tmach.agreemap	$⊢ φ \to A = (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
6		tmach.agreement	$⊢ φ \to \forall z \in T \forall y \in A (z) S (y) = S (z)$
7	1 2 3 4 5 6	tmachlem-extpcover	$⊢ φ \to \exists a \in (𝒫 ran A \cap Fin) ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a$
8		df-rex	$⊢ \exists a \in (𝒫 ran A \cap Fin) ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a \leftrightarrow \exists a (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)$
9	7 8	sylib	$⊢ φ \to \exists a (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)$
10		simprl	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to a \in (𝒫 ran A \cap Fin)$
11	10	elin1d	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to a \in 𝒫 ran A$
12	11	elpwid	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to a \subseteq ran A$
13	10	elin2d	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to a \in Fin$
14	1 2 3 4 5 6	tmachlem-tpbase	$⊢ φ \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = T$
15	14	adantr	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = T$
16		simprr	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a$
17	15 16	eqtr3d	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to T = ⋃ a$
18	12 13 17	3jca	$⊢ (φ \land (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a)) \to (a \subseteq ran A \land a \in Fin \land T = ⋃ a)$
19	18	ex	$⊢ φ \to ((a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a) \to (a \subseteq ran A \land a \in Fin \land T = ⋃ a))$
20	19	eximdv	$⊢ φ \to (\exists a (a \in (𝒫 ran A \cap Fin) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a) \to \exists a (a \subseteq ran A \land a \in Fin \land T = ⋃ a))$
21	9 20	mpd	$⊢ φ \to \exists a (a \subseteq ran A \land a \in Fin \land T = ⋃ a)$

Metamath Proof Explorer

Theorem tmachlem-exagreecover

Proof