Theorem mndind

Description: Induction in a monoid. In this theorem, ps ( x ) is the "generic" proposition to be be proved (the first four hypotheses tell its values at y, y+z, 0, A respectively). The two induction hypotheses mndind.i1 and mndind.i2 tell that it is true at 0, that if it is true at y then it is true at y+z (provided z is in G ). The hypothesis mndind.k tells that G is generating. (Contributed by SO, 14-Jul-2018)

	Ref	Expression
Hypotheses	mndind.ch	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
	mndind.th	$$⊢x=y\underset{\dot{}}{+}z\to \left(\psi \leftrightarrow \theta \right)$$
	mndind.ta	$$⊢x=\underset{\dot{}}{0}\to \left(\psi \leftrightarrow \tau \right)$$
	mndind.et	$$⊢x=A\to \left(\psi \leftrightarrow \eta \right)$$
	mndind.0g	$$⊢\underset{\dot{}}{0}=0_M$$
	mndind.pg	$$⊢\underset{\dot{}}{+}={+}_M$$
	mndind.b	$$⊢B={\mathrm{Base}}_M$$
	mndind.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndind.g	$$⊢\phi \to G\subseteq B$$
	mndind.k	$$⊢\phi \to B=\mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)\left(G\right)$$
	mndind.i1	$$⊢\phi \to \tau$$
	mndind.i2	$$⊢\left(\left(\phi \wedge y\in B\wedge z\in G\right)\wedge \chi \right)\to \theta$$
	mndind.a	$$⊢\phi \to A\in B$$
Assertion	mndind	$$⊢\phi \to \eta$$

Proof

Step	Hyp	Ref	Expression
1		mndind.ch	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
2		mndind.th	$$⊢x=y\underset{\dot{}}{+}z\to \left(\psi \leftrightarrow \theta \right)$$
3		mndind.ta	$$⊢x=\underset{\dot{}}{0}\to \left(\psi \leftrightarrow \tau \right)$$
4		mndind.et	$$⊢x=A\to \left(\psi \leftrightarrow \eta \right)$$
5		mndind.0g	$$⊢\underset{\dot{}}{0}=0_M$$
6		mndind.pg	$$⊢\underset{\dot{}}{+}={+}_M$$
7		mndind.b	$$⊢B={\mathrm{Base}}_M$$
8		mndind.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
9		mndind.g	$$⊢\phi \to G\subseteq B$$
10		mndind.k	$$⊢\phi \to B=\mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)\left(G\right)$$
11		mndind.i1	$$⊢\phi \to \tau$$
12		mndind.i2	$$⊢\left(\left(\phi \wedge y\in B\wedge z\in G\right)\wedge \chi \right)\to \theta$$
13		mndind.a	$$⊢\phi \to A\in B$$
14	7 5	mndidcl	$$⊢M\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
15	8 14	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
16	3	sbcieg	$$⊢\underset{\dot{}}{0}\in B\to \left(\underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi \leftrightarrow \tau \right)$$
17	15 16	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi \leftrightarrow \tau \right)$$
18	11 17	mpbird	$$⊢\phi \to \underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi$$
19		dfsbcq	$$⊢a=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi \right)$$
20		oveq1	$$⊢a=\underset{\dot{}}{0}\to a\underset{\dot{}}{+}A=\underset{\dot{}}{0}\underset{\dot{}}{+}A$$
21	20	sbceq1d	$$⊢a=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)$$
22	19 21	imbi12d	$$⊢a=\underset{\dot{}}{0}\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
23	7	submacs	$$⊢M\in \mathrm{Mnd}\to \mathrm{SubMnd}\left(M\right)\in \mathrm{ACS}\left(B\right)$$
24	8 23	syl	$$⊢\phi \to \mathrm{SubMnd}\left(M\right)\in \mathrm{ACS}\left(B\right)$$
25	24	acsmred	$$⊢\phi \to \mathrm{SubMnd}\left(M\right)\in \mathrm{Moore}\left(B\right)$$
26		eleq1w	$$⊢y=a\to \left(y\in B\leftrightarrow a\in B\right)$$
27	26	anbi2d	$$⊢y=a\to \left(\left(\left(\phi \wedge b\in G\right)\wedge y\in B\right)\leftrightarrow \left(\left(\phi \wedge b\in G\right)\wedge a\in B\right)\right)$$
28		vex	$$⊢y\in \mathrm{V}$$
29	28 1	sbcie	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \leftrightarrow \chi$$
30		dfsbcq	$$⊢y=a\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
31	29 30	syl5bbr	$$⊢y=a\to \left(\chi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
32		oveq1	$$⊢y=a\to y\underset{\dot{}}{+}b=a\underset{\dot{}}{+}b$$
33	32	sbceq1d	$$⊢y=a\to \left(\underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
34	31 33	imbi12d	$$⊢y=a\to \left(\left(\chi \to \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
35	27 34	imbi12d	$$⊢y=a\to \left(\left(\left(\left(\phi \wedge b\in G\right)\wedge y\in B\right)\to \left(\chi \to \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right)\leftrightarrow \left(\left(\left(\phi \wedge b\in G\right)\wedge a\in B\right)\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
36		eleq1w	$$⊢z=b\to \left(z\in G\leftrightarrow b\in G\right)$$
37	36	anbi2d	$$⊢z=b\to \left(\left(\phi \wedge z\in G\right)\leftrightarrow \left(\phi \wedge b\in G\right)\right)$$
38	37	anbi1d	$$⊢z=b\to \left(\left(\left(\phi \wedge z\in G\right)\wedge y\in B\right)\leftrightarrow \left(\left(\phi \wedge b\in G\right)\wedge y\in B\right)\right)$$
39		ovex	$$⊢y\underset{\dot{}}{+}z\in \mathrm{V}$$
40	39 2	sbcie	$$⊢\underset{\dot{}}{[}\left(y\underset{\dot{}}{+}z\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \theta$$
41		oveq2	$$⊢z=b\to y\underset{\dot{}}{+}z=y\underset{\dot{}}{+}b$$
42	41	sbceq1d	$$⊢z=b\to \left(\underset{\dot{}}{[}\left(y\underset{\dot{}}{+}z\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
43	40 42	syl5bbr	$$⊢z=b\to \left(\theta \leftrightarrow \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
44	43	imbi2d	$$⊢z=b\to \left(\left(\chi \to \theta \right)\leftrightarrow \left(\chi \to \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
45	38 44	imbi12d	$$⊢z=b\to \left(\left(\left(\left(\phi \wedge z\in G\right)\wedge y\in B\right)\to \left(\chi \to \theta \right)\right)\leftrightarrow \left(\left(\left(\phi \wedge b\in G\right)\wedge y\in B\right)\to \left(\chi \to \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)$$
46	12	ex	$$⊢\left(\phi \wedge y\in B\wedge z\in G\right)\to \left(\chi \to \theta \right)$$
47	46	3expa	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge z\in G\right)\to \left(\chi \to \theta \right)$$
48	47	an32s	$$⊢\left(\left(\phi \wedge z\in G\right)\wedge y\in B\right)\to \left(\chi \to \theta \right)$$
49	45 48	chvarvv	$$⊢\left(\left(\phi \wedge b\in G\right)\wedge y\in B\right)\to \left(\chi \to \underset{\dot{}}{[}\left(y\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
50	35 49	chvarvv	$$⊢\left(\left(\phi \wedge b\in G\right)\wedge a\in B\right)\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
51	50	ralrimiva	$$⊢\left(\phi \wedge b\in G\right)\to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)$$
52	9 51	ssrabdv	$$⊢\phi \to G\subseteq \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}$$
53	7 6 5	mndrid	$$⊢\left(M\in \mathrm{Mnd}\wedge a\in B\right)\to a\underset{\dot{}}{+}\underset{\dot{}}{0}=a$$
54	8 53	sylan	$$⊢\left(\phi \wedge a\in B\right)\to a\underset{\dot{}}{+}\underset{\dot{}}{0}=a$$
55	54	sbceq1d	$$⊢\left(\phi \wedge a\in B\right)\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \right)$$
56	55	biimprd	$$⊢\left(\phi \wedge a\in B\right)\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \right)$$
57	56	ralrimiva	$$⊢\phi \to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \right)$$
58		simprrl	$$⊢\left(\phi \wedge \left(\left(c\in B\wedge d\in B\right)\wedge \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)\right)\to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)$$
59	8	ad2antrr	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to M\in \mathrm{Mnd}$$
60		simpr	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to b\in B$$
61		simplrl	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to c\in B$$
62	7 6	mndcl	$$⊢\left(M\in \mathrm{Mnd}\wedge b\in B\wedge c\in B\right)\to b\underset{\dot{}}{+}c\in B$$
63	59 60 61 62	syl3anc	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to b\underset{\dot{}}{+}c\in B$$
64		simpr	$$⊢\left(\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\wedge a=b\underset{\dot{}}{+}c\right)\to a=b\underset{\dot{}}{+}c$$
65	64	sbceq1d	$$⊢\left(\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\wedge a=b\underset{\dot{}}{+}c\right)\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)$$
66		oveq1	$$⊢a=b\underset{\dot{}}{+}c\to a\underset{\dot{}}{+}d=\left(b\underset{\dot{}}{+}c\right)\underset{\dot{}}{+}d$$
67		simplrr	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to d\in B$$
68	7 6	mndass	$$⊢\left(M\in \mathrm{Mnd}\wedge \left(b\in B\wedge c\in B\wedge d\in B\right)\right)\to \left(b\underset{\dot{}}{+}c\right)\underset{\dot{}}{+}d=b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)$$
69	59 60 61 67 68	syl13anc	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to \left(b\underset{\dot{}}{+}c\right)\underset{\dot{}}{+}d=b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)$$
70	66 69	sylan9eqr	$$⊢\left(\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\wedge a=b\underset{\dot{}}{+}c\right)\to a\underset{\dot{}}{+}d=b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)$$
71	70	sbceq1d	$$⊢\left(\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\wedge a=b\underset{\dot{}}{+}c\right)\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
72	65 71	imbi12d	$$⊢\left(\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\wedge a=b\underset{\dot{}}{+}c\right)\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
73	63 72	rspcdv	$$⊢\left(\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\wedge b\in B\right)\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\to \left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
74	73	ralrimdva	$$⊢\left(\phi \wedge \left(c\in B\wedge d\in B\right)\right)\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\to \forall b\in B\left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
75	74	impr	$$⊢\left(\phi \wedge \left(\left(c\in B\wedge d\in B\right)\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)\to \forall b\in B\left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
76		oveq1	$$⊢b=a\to b\underset{\dot{}}{+}c=a\underset{\dot{}}{+}c$$
77	76	sbceq1d	$$⊢b=a\to \left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)$$
78		oveq1	$$⊢b=a\to b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)=a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)$$
79	78	sbceq1d	$$⊢b=a\to \left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
80	77 79	imbi12d	$$⊢b=a\to \left(\left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
81	80	cbvralvw	$$⊢\forall b\in B\left(\underset{\dot{}}{[}\left(b\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(b\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
82	75 81	sylib	$$⊢\left(\phi \wedge \left(\left(c\in B\wedge d\in B\right)\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)\to \forall a\in B\left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
83	82	adantrrl	$$⊢\left(\phi \wedge \left(\left(c\in B\wedge d\in B\right)\wedge \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)\right)\to \forall a\in B\left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
84		imim1	$$⊢\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\to \left(\left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
85	84	ral2imi	$$⊢\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\to \left(\forall a\in B\left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
86	58 83 85	sylc	$$⊢\left(\phi \wedge \left(\left(c\in B\wedge d\in B\right)\wedge \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)\right)\right)\to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
87		oveq2	$$⊢b=\underset{\dot{}}{0}\to a\underset{\dot{}}{+}b=a\underset{\dot{}}{+}\underset{\dot{}}{0}$$
88	87	sbceq1d	$$⊢b=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \right)$$
89	88	imbi2d	$$⊢b=\underset{\dot{}}{0}\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
90	89	ralbidv	$$⊢b=\underset{\dot{}}{0}\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\underset{\dot{}}{0}\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
91		oveq2	$$⊢b=c\to a\underset{\dot{}}{+}b=a\underset{\dot{}}{+}c$$
92	91	sbceq1d	$$⊢b=c\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)$$
93	92	imbi2d	$$⊢b=c\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
94	93	ralbidv	$$⊢b=c\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}c\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
95		oveq2	$$⊢b=d\to a\underset{\dot{}}{+}b=a\underset{\dot{}}{+}d$$
96	95	sbceq1d	$$⊢b=d\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)$$
97	96	imbi2d	$$⊢b=d\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
98	97	ralbidv	$$⊢b=d\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}d\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
99		oveq2	$$⊢b=c\underset{\dot{}}{+}d\to a\underset{\dot{}}{+}b=a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)$$
100	99	sbceq1d	$$⊢b=c\underset{\dot{}}{+}d\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)$$
101	100	imbi2d	$$⊢b=c\underset{\dot{}}{+}d\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
102	101	ralbidv	$$⊢b=c\underset{\dot{}}{+}d\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}\left(c\underset{\dot{}}{+}d\right)\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
103	7 6 5 8 57 86 90 94 98 102	issubmd	$$⊢\phi \to \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}\in \mathrm{SubMnd}\left(M\right)$$
104		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)=\mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)$$
105	104	mrcsscl	$$⊢\left(\mathrm{SubMnd}\left(M\right)\in \mathrm{Moore}\left(B\right)\wedge G\subseteq \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}\wedge \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}\in \mathrm{SubMnd}\left(M\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)\left(G\right)\subseteq \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}$$
106	25 52 103 105	syl3anc	$$⊢\phi \to \mathrm{mrCls}\left(\mathrm{SubMnd}\left(M\right)\right)\left(G\right)\subseteq \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}$$
107	10 106	eqsstrd	$$⊢\phi \to B\subseteq \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}$$
108	107 13	sseldd	$$⊢\phi \to A\in \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}$$
109		oveq2	$$⊢b=A\to a\underset{\dot{}}{+}b=a\underset{\dot{}}{+}A$$
110	109	sbceq1d	$$⊢b=A\to \left(\underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)$$
111	110	imbi2d	$$⊢b=A\to \left(\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
112	111	ralbidv	$$⊢b=A\to \left(\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
113	112	elrab	$$⊢A\in \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}\leftrightarrow \left(A\in B\wedge \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)\right)$$
114	113	simprbi	$$⊢A\in \left\{b\in B|\forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}b\right)/x\underset{\dot{}}{]}\psi \right)\right\}\to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)$$
115	108 114	syl	$$⊢\phi \to \forall a\in B\left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(a\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)$$
116	22 115 15	rspcdva	$$⊢\phi \to \left(\underset{\dot{}}{[}\underset{\dot{}}{0}/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \right)$$
117	18 116	mpd	$$⊢\phi \to \underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi$$
118	7 6 5	mndlid	$$⊢\left(M\in \mathrm{Mnd}\wedge A\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}A=A$$
119	8 13 118	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}A=A$$
120	119	sbceq1d	$$⊢\phi \to \left(\underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
121	4	sbcieg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta \right)$$
122	13 121	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta \right)$$
123	120 122	bitrd	$$⊢\phi \to \left(\underset{\dot{}}{[}\left(\underset{\dot{}}{0}\underset{\dot{}}{+}A\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \eta \right)$$
124	117 123	mpbid	$$⊢\phi \to \eta$$