tmachlem-agreefin

Description: Any agreement set has a finite (singleton) list of possible scans. (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-agreefin	$⊢ (φ \land b \in ran A) \to S [b] \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		funmpt	$⊢ Fun (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
8	5	funeqd	$⊢ φ \to (Fun A \leftrightarrow Fun (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}))$
9	7 8	mpbiri	$⊢ φ \to Fun A$
10		elrnrexdm	$⊢ Fun A \to (b \in ran A \to \exists a \in dom A b = A (a))$
11	9 10	syl	$⊢ φ \to (b \in ran A \to \exists a \in dom A b = A (a))$
12	11	imp	$⊢ (φ \land b \in ran A) \to \exists a \in dom A b = A (a)$
13		simprr	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to b = A (a)$
14	13	imaeq2d	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to S [b] = S [A (a)]$
15		simpll	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to φ$
16		simprl	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to a \in dom A$
17	5	dmeqd	$⊢ φ \to dom A = dom (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
18	1 2 3 4 5 6	tmachlem-extapes	$⊢ φ \to T \in V$
19		ssrab2	$⊢ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \subseteq T$
20	19	a1i	$⊢ φ \to \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \subseteq T$
21	18 20	ssexd	$⊢ φ \to \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V$
22	21	ralrimivw	$⊢ φ \to \forall z \in T \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V$
23		dmmptg	$⊢ \forall z \in T \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} \in V \to dom (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}) = T$
24	22 23	syl	$⊢ φ \to dom (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\}) = T$
25	17 24	eqtrd	$⊢ φ \to dom A = T$
26	25	ad2antrr	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to dom A = T$
27	16 26	eleqtrd	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to a \in T$
28	1 2 3 4 5 6	tmachlem-agreesn	$⊢ (φ \land a \in T) \to S [A (a)] = \{S (a)\}$
29	15 27 28	syl2anc	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to S [A (a)] = \{S (a)\}$
30	14 29	eqtrd	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to S [b] = \{S (a)\}$
31		snfi	$⊢ \{S (a)\} \in Fin$
32	30 31	eqeltrdi	$⊢ ((φ \land b \in ran A) \land (a \in dom A \land b = A (a))) \to S [b] \in Fin$
33	12 32	rexlimddv	$⊢ (φ \land b \in ran A) \to S [b] \in Fin$

Metamath Proof Explorer

Theorem tmachlem-agreefin

Proof