tmachlem-extpcover

Description: Product topology of tapes admits finite cover. (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-extpcover	$⊢ φ \to \exists a \in (𝒫 ran A \cap Fin) ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ 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-tpcomp	$⊢ φ \to \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \in Comp$
8	1 2 3 4 5 6	tmachlem-extapes	$⊢ φ \to T \in V$
9		ssrab2	$⊢ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \subseteq T$
10	9	a1i	$⊢ φ \to \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \subseteq T$
11	8 10	ssexd	$⊢ φ \to \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V$
12	11	ralrimivw	$⊢ φ \to \forall z \in T \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V$
13		nfcv	$⊢ \underline{Ⅎ} z T$
14	13	mptfnf	$⊢ \forall z \in T \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V \leftrightarrow (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}) Fn T$
15	12 14	sylib	$⊢ φ \to (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}) Fn T$
16	5	fneq1d	$⊢ φ \to (A Fn T \leftrightarrow (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}) Fn T)$
17	15 16	mpbird	$⊢ φ \to A Fn T$
18	1 2 3 4 5 6	tmachlem-tpopen2	$⊢ (φ \land b \in T) \to A (b) \in \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
19	18	ralrimiva	$⊢ φ \to \forall b \in T A (b) \in \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
20		fnfvrnss	$⊢ (A Fn T \land \forall b \in T A (b) \in \prod_{𝑡} ((i \in I ⟼ 𝒫 U))) \to ran A \subseteq \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
21	17 19 20	syl2anc	$⊢ φ \to ran A \subseteq \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
22	1 2 3 4 5 6	tmachlem-tpbase	$⊢ φ \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = T$
23	1 2 3 4 5 6	tmachlem-exlargecover	$⊢ φ \to ⋃ ran A = T$
24	22 23	eqtr4d	$⊢ φ \to ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ ran A$
25		eqid	$⊢ ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U))$
26	25	cmpcov	$⊢ (\prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \in Comp \land ran A \subseteq \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) \land ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ ran A) \to \exists a \in (𝒫 ran A \cap Fin) ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a$
27	7 21 24 26	syl3anc	$⊢ φ \to \exists a \in (𝒫 ran A \cap Fin) ⋃ \prod_{𝑡} ((i \in I ⟼ 𝒫 U)) = ⋃ a$

Metamath Proof Explorer

Theorem tmachlem-extpcover

Proof