tmachlem-franscan

Description: There is a finite number of different scan sets. (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-franscan	$⊢ φ \to ran S \in Fin$

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	4	ffnd	$⊢ φ \to S Fn T$
8		fnima	$⊢ S Fn T \to S [T] = ran S$
9	7 8	syl	$⊢ φ \to S [T] = ran S$
10	1 2 3 4 5 6	tmachlem-exagreecover	$⊢ φ \to \exists a (a \subseteq ran A \land a \in Fin \land T = ⋃ a)$
11		simpr3	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to T = ⋃ a$
12	11	imaeq2d	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to S [T] = S [⋃ a]$
13		imauni	$⊢ S [⋃ a] = ⋃_{i \in a} S [i]$
14	12 13	eqtrdi	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to S [T] = ⋃_{i \in a} S [i]$
15		simpr2	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to a \in Fin$
16		simpll	$⊢ ((φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \land i \in a) \to φ$
17		simplr1	$⊢ ((φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \land i \in a) \to a \subseteq ran A$
18		simpr	$⊢ ((φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \land i \in a) \to i \in a$
19	17 18	sseldd	$⊢ ((φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \land i \in a) \to i \in ran A$
20	1 2 3 4 5 6	tmachlem-agreefin	$⊢ (φ \land i \in ran A) \to S [i] \in Fin$
21	16 19 20	syl2anc	$⊢ ((φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \land i \in a) \to S [i] \in Fin$
22	21	ralrimiva	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to \forall i \in a S [i] \in Fin$
23		iunfi	$⊢ (a \in Fin \land \forall i \in a S [i] \in Fin) \to ⋃_{i \in a} S [i] \in Fin$
24	15 22 23	syl2anc	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to ⋃_{i \in a} S [i] \in Fin$
25	14 24	eqeltrd	$⊢ (φ \land (a \subseteq ran A \land a \in Fin \land T = ⋃ a)) \to S [T] \in Fin$
26	10 25	exlimddv	$⊢ φ \to S [T] \in Fin$
27	9 26	eqeltrrd	$⊢ φ \to ran S \in Fin$

Metamath Proof Explorer

Theorem tmachlem-franscan

Proof