tmachlem-agreeprod

Description: Agreement set can be written as infinite product of acceptable values for tape's cells. (Contributed by Ender Ting, 27-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-agreeprod	$⊢ (φ \land a \in T) \to A (a) = \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U)$

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		fveq2	$⊢ z = a \to S (z) = S (a)$
8	7	reseq2d	$⊢ z = a \to {y ↾}_{S (z)} = {y ↾}_{S (a)}$
9		id	$⊢ z = a \to z = a$
10	9 7	reseq12d	$⊢ z = a \to {z ↾}_{S (z)} = {a ↾}_{S (a)}$
11	8 10	eqeq12d	$⊢ z = a \to ({y ↾}_{S (z)} = {z ↾}_{S (z)} \leftrightarrow {y ↾}_{S (a)} = {a ↾}_{S (a)})$
12	11	rabbidv	$⊢ z = a \to \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\} = \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\}$
13	5	adantr	$⊢ (φ \land a \in T) \to A = (z \in T ⟼ \{y \in T \| {y ↾}_{S (z)} = {z ↾}_{S (z)}\})$
14		simpr	$⊢ (φ \land a \in T) \to a \in T$
15	1 2 3 4 5 6	tmachlem-extapes	$⊢ φ \to T \in V$
16	15	adantr	$⊢ (φ \land a \in T) \to T \in V$
17		ssrab2	$⊢ \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\} \subseteq T$
18	17	a1i	$⊢ (φ \land a \in T) \to \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\} \subseteq T$
19	16 18	ssexd	$⊢ (φ \land a \in T) \to \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\} \in V$
20	12 13 14 19	fvmptd4	$⊢ (φ \land a \in T) \to A (a) = \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\}$
21		snfi	$⊢ \{a (i)\} \in Fin$
22	21	a1i	$⊢ ((φ \land a \in T) \land i \in I) \to \{a (i)\} \in Fin$
23	1	ad2antrr	$⊢ ((φ \land a \in T) \land i \in I) \to U \in Fin$
24	22 23	ifcld	$⊢ ((φ \land a \in T) \land i \in I) \to if (i \in S (a), \{a (i)\}, U) \in Fin$
25	24	ralrimiva	$⊢ (φ \land a \in T) \to \forall i \in I if (i \in S (a), \{a (i)\}, U) \in Fin$
26		ixpssmapg	$⊢ \forall i \in I if (i \in S (a), \{a (i)\}, U) \in Fin \to \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \subseteq {⋃_{i \in I} if (i \in S (a), \{a (i)\}, U)}^{I}$
27	25 26	syl	$⊢ (φ \land a \in T) \to \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \subseteq {⋃_{i \in I} if (i \in S (a), \{a (i)\}, U)}^{I}$
28		ifssun	$⊢ if (i \in S (a), \{a (i)\}, U) \subseteq \{a (i)\} \cup U$
29	3	eleq2d	$⊢ φ \to (a \in T \leftrightarrow a \in (U^{I}))$
30	29	biimpd	$⊢ φ \to (a \in T \to a \in (U^{I}))$
31	30	imp	$⊢ (φ \land a \in T) \to a \in (U^{I})$
32		elmapi	$⊢ a \in (U^{I}) \to a : I ⟶ U$
33	31 32	syl	$⊢ (φ \land a \in T) \to a : I ⟶ U$
34	33	ffvelcdmda	$⊢ ((φ \land a \in T) \land i \in I) \to a (i) \in U$
35	34	snssd	$⊢ ((φ \land a \in T) \land i \in I) \to \{a (i)\} \subseteq U$
36		ssequn1	$⊢ \{a (i)\} \subseteq U \leftrightarrow \{a (i)\} \cup U = U$
37	35 36	sylib	$⊢ ((φ \land a \in T) \land i \in I) \to \{a (i)\} \cup U = U$
38	28 37	sseqtrid	$⊢ ((φ \land a \in T) \land i \in I) \to if (i \in S (a), \{a (i)\}, U) \subseteq U$
39	38	iunssd	$⊢ (φ \land a \in T) \to ⋃_{i \in I} if (i \in S (a), \{a (i)\}, U) \subseteq U$
40		mapss	$⊢ (U \in Fin \land ⋃_{i \in I} if (i \in S (a), \{a (i)\}, U) \subseteq U) \to {⋃_{i \in I} if (i \in S (a), \{a (i)\}, U)}^{I} \subseteq U^{I}$
41	1 39 40	syl2an2r	$⊢ (φ \land a \in T) \to {⋃_{i \in I} if (i \in S (a), \{a (i)\}, U)}^{I} \subseteq U^{I}$
42	27 41	sstrd	$⊢ (φ \land a \in T) \to \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \subseteq U^{I}$
43	3	adantr	$⊢ (φ \land a \in T) \to T = U^{I}$
44	42 43	sseqtrrd	$⊢ (φ \land a \in T) \to \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \subseteq T$
45		simplr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to i \in S (a)$
46		simpr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to (i \in S (a) \to y (i) = a (i))$
47	45 46	mpd	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to y (i) = a (i)$
48		fvex	$⊢ y (i) \in V$
49	48	elsn	$⊢ y (i) \in \{a (i)\} \leftrightarrow y (i) = a (i)$
50	47 49	sylibr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to y (i) \in \{a (i)\}$
51	45	iftrued	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to if (i \in S (a), \{a (i)\}, U) = \{a (i)\}$
52	50 51	eleqtrrd	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in S (a) \to y (i) = a (i))) \to y (i) \in if (i \in S (a), \{a (i)\}, U)$
53	52	ex	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to ((i \in S (a) \to y (i) = a (i)) \to y (i) \in if (i \in S (a), \{a (i)\}, U))$
54	53	a1dd	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to ((i \in S (a) \to y (i) = a (i)) \to (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)))$
55	4	ffvelcdmda	$⊢ (φ \land a \in T) \to S (a) \in (𝒫 I \cap Fin)$
56	55	elin1d	$⊢ (φ \land a \in T) \to S (a) \in 𝒫 I$
57	56	elpwid	$⊢ (φ \land a \in T) \to S (a) \subseteq I$
58	57	adantr	$⊢ ((φ \land a \in T) \land y \in T) \to S (a) \subseteq I$
59	58	sselda	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to i \in I$
60	59	adantr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to i \in I$
61		simpr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))$
62	60 61	mpd	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to y (i) \in if (i \in S (a), \{a (i)\}, U)$
63		simplr	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to i \in S (a)$
64	63	iftrued	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to if (i \in S (a), \{a (i)\}, U) = \{a (i)\}$
65	62 64	eleqtrd	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to y (i) \in \{a (i)\}$
66	65	elsnd	$⊢ ((((φ \land a \in T) \land y \in T) \land i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to y (i) = a (i)$
67	66	ex	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to ((i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)) \to y (i) = a (i))$
68	67	a1dd	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to ((i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)) \to (i \in S (a) \to y (i) = a (i)))$
69	54 68	impbid	$⊢ (((φ \land a \in T) \land y \in T) \land i \in S (a)) \to ((i \in S (a) \to y (i) = a (i)) \leftrightarrow (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)))$
70	3	eleq2d	$⊢ φ \to (y \in T \leftrightarrow y \in (U^{I}))$
71	70	biimpd	$⊢ φ \to (y \in T \to y \in (U^{I}))$
72	71	adantr	$⊢ (φ \land a \in T) \to (y \in T \to y \in (U^{I}))$
73	72	imp	$⊢ ((φ \land a \in T) \land y \in T) \to y \in (U^{I})$
74		elmapi	$⊢ y \in (U^{I}) \to y : I ⟶ U$
75	73 74	syl	$⊢ ((φ \land a \in T) \land y \in T) \to y : I ⟶ U$
76	75	adantr	$⊢ (((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \to y : I ⟶ U$
77	76	ffvelcdmda	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land i \in I) \to y (i) \in U$
78		simplr	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land i \in I) \to \neg i \in S (a)$
79	78	iffalsed	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land i \in I) \to if (i \in S (a), \{a (i)\}, U) = U$
80	77 79	eleqtrrd	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land i \in I) \to y (i) \in if (i \in S (a), \{a (i)\}, U)$
81	80	ex	$⊢ (((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \to (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))$
82	81	a1d	$⊢ (((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \to ((i \in S (a) \to y (i) = a (i)) \to (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)))$
83		simplr	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to \neg i \in S (a)$
84	83	pm2.21d	$⊢ ((((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \land (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U))) \to (i \in S (a) \to y (i) = a (i))$
85	84	ex	$⊢ (((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \to ((i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)) \to (i \in S (a) \to y (i) = a (i)))$
86	82 85	impbid	$⊢ (((φ \land a \in T) \land y \in T) \land \neg i \in S (a)) \to ((i \in S (a) \to y (i) = a (i)) \leftrightarrow (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)))$
87	69 86	pm2.61dan	$⊢ ((φ \land a \in T) \land y \in T) \to ((i \in S (a) \to y (i) = a (i)) \leftrightarrow (i \in I \to y (i) \in if (i \in S (a), \{a (i)\}, U)))$
88	87	ralbidv2	$⊢ ((φ \land a \in T) \land y \in T) \to (\forall i \in S (a) y (i) = a (i) \leftrightarrow \forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U))$
89	71	imp	$⊢ (φ \land y \in T) \to y \in (U^{I})$
90		elmapfn	$⊢ y \in (U^{I}) \to y Fn I$
91	89 90	syl	$⊢ (φ \land y \in T) \to y Fn I$
92	91	adantlr	$⊢ ((φ \land a \in T) \land y \in T) \to y Fn I$
93	92	biantrurd	$⊢ ((φ \land a \in T) \land y \in T) \to (\forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U) \leftrightarrow (y Fn I \land \forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U)))$
94	88 93	bitr2d	$⊢ ((φ \land a \in T) \land y \in T) \to ((y Fn I \land \forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U)) \leftrightarrow \forall i \in S (a) y (i) = a (i))$
95		vex	$⊢ y \in V$
96	95	elixp	$⊢ y \in \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \leftrightarrow (y Fn I \land \forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U))$
97	96	a1i	$⊢ ((φ \land a \in T) \land y \in T) \to (y \in \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \leftrightarrow (y Fn I \land \forall i \in I y (i) \in if (i \in S (a), \{a (i)\}, U)))$
98		elmapfn	$⊢ a \in (U^{I}) \to a Fn I$
99	31 98	syl	$⊢ (φ \land a \in T) \to a Fn I$
100	99	adantr	$⊢ ((φ \land a \in T) \land y \in T) \to a Fn I$
101		fvreseq	$⊢ ((y Fn I \land a Fn I) \land S (a) \subseteq I) \to ({y ↾}_{S (a)} = {a ↾}_{S (a)} \leftrightarrow \forall i \in S (a) y (i) = a (i))$
102	92 100 58 101	syl21anc	$⊢ ((φ \land a \in T) \land y \in T) \to ({y ↾}_{S (a)} = {a ↾}_{S (a)} \leftrightarrow \forall i \in S (a) y (i) = a (i))$
103	94 97 102	3bitr4d	$⊢ ((φ \land a \in T) \land y \in T) \to (y \in \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) \leftrightarrow {y ↾}_{S (a)} = {a ↾}_{S (a)})$
104	44 103	eqrrabd	$⊢ (φ \land a \in T) \to \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U) = \{y \in T \| {y ↾}_{S (a)} = {a ↾}_{S (a)}\}$
105	20 104	eqtr4d	$⊢ (φ \land a \in T) \to A (a) = \underset{i \in I}{⨉} if (i \in S (a), \{a (i)\}, U)$

Metamath Proof Explorer

Theorem tmachlem-agreeprod

Proof