Theorem msrid

Description: The reduct of a statement is itself. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mstaval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
	mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
Assertion	msrid	$$⊢X\in S\to R\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
3		eqid	$$⊢\mathrm{mPreSt}\left(T\right)=\mathrm{mPreSt}\left(T\right)$$
4	3 1	msrf	$$⊢R:\mathrm{mPreSt}\left(T\right)⟶\mathrm{mPreSt}\left(T\right)$$
5		ffn	$$⊢R:\mathrm{mPreSt}\left(T\right)⟶\mathrm{mPreSt}\left(T\right)\to RFn\mathrm{mPreSt}\left(T\right)$$
6		fvelrnb	$$⊢RFn\mathrm{mPreSt}\left(T\right)\to \left(X\in \mathrm{ran}R\leftrightarrow \exists s\in \mathrm{mPreSt}\left(T\right)R\left(s\right)=X\right)$$
7	4 5 6	mp2b	$$⊢X\in \mathrm{ran}R\leftrightarrow \exists s\in \mathrm{mPreSt}\left(T\right)R\left(s\right)=X$$
8	3	mpst123	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to s=⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
9	8	fveq2d	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(s\right)=R\left(⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)$$
10		id	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to s\in \mathrm{mPreSt}\left(T\right)$$
11	8 10	eqeltrrd	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to ⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\in \mathrm{mPreSt}\left(T\right)$$
12		eqid	$$⊢\mathrm{mVars}\left(T\right)=\mathrm{mVars}\left(T\right)$$
13		eqid	$$⊢\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]=\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]$$
14	12 3 1 13	msrval	$$⊢⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\in \mathrm{mPreSt}\left(T\right)\to R\left(⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
15	11 14	syl	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
16	9 15	eqtrd	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(s\right)=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
17	4	ffvelrni	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(s\right)\in \mathrm{mPreSt}\left(T\right)$$
18	16 17	eqeltrrd	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to ⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\in \mathrm{mPreSt}\left(T\right)$$
19	12 3 1 13	msrval	$$⊢⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\in \mathrm{mPreSt}\left(T\right)\to R\left(⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)=⟨\left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
20	18 19	syl	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)=⟨\left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
21		inass	$$⊢\left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)=1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)$$
22		inidm	$$⊢\left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)=\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]$$
23	22	ineq2i	$$⊢1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)=1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)$$
24	21 23	eqtri	$$⊢\left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)=1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)$$
25	24	a1i	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to \left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)=1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)$$
26	25	oteq1d	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to ⟨\left(1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
27	20 26	eqtrd	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)=⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩$$
28	16	fveq2d	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(R\left(s\right)\right)=R\left(⟨1^{st}\left(1^{st}\left(s\right)\right)\cap \left(\bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\times \bigcup \mathrm{mVars}\left(T\right)\left[2^{nd}\left(1^{st}\left(s\right)\right)\cup \left\{2^{nd}\left(s\right)\right\}\right]\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\right)$$
29	27 28 16	3eqtr4d	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to R\left(R\left(s\right)\right)=R\left(s\right)$$
30		fveq2	$$⊢R\left(s\right)=X\to R\left(R\left(s\right)\right)=R\left(X\right)$$
31		id	$$⊢R\left(s\right)=X\to R\left(s\right)=X$$
32	30 31	eqeq12d	$$⊢R\left(s\right)=X\to \left(R\left(R\left(s\right)\right)=R\left(s\right)\leftrightarrow R\left(X\right)=X\right)$$
33	29 32	syl5ibcom	$$⊢s\in \mathrm{mPreSt}\left(T\right)\to \left(R\left(s\right)=X\to R\left(X\right)=X\right)$$
34	33	rexlimiv	$$⊢\exists s\in \mathrm{mPreSt}\left(T\right)R\left(s\right)=X\to R\left(X\right)=X$$
35	7 34	sylbi	$$⊢X\in \mathrm{ran}R\to R\left(X\right)=X$$
36	1 2	mstaval	$$⊢S=\mathrm{ran}R$$
37	35 36	eleq2s	$$⊢X\in S\to R\left(X\right)=X$$