Theorem msrf

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

	Ref	Expression
Hypotheses	mpstssv.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
	msrf.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
Assertion	msrf	$$⊢R:P⟶P$$

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
2		msrf.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
3		otex	$$⊢⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(T\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\in \mathrm{V}$$
4	3	csbex	$$⊢⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(T\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\in \mathrm{V}$$
5	4	csbex	$$⊢⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(T\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\in \mathrm{V}$$
6		eqid	$$⊢\mathrm{mVars}\left(T\right)=\mathrm{mVars}\left(T\right)$$
7	6 1 2	msrfval	$$⊢R=\left(s\in P⟼⦋2^{nd}\left(1^{st}\left(s\right)\right)/h⦌⦋2^{nd}\left(s\right)/a⦌⟨1^{st}\left(1^{st}\left(s\right)\right)\cap ⦋\bigcup \mathrm{mVars}\left(T\right)\left[h\cup \left\{a\right\}\right]/z⦌\left(z\times z\right),h,a⟩\right)$$
8	5 7	fnmpti	$$⊢RFnP$$
9	1	mpst123	$$⊢s\in P\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)⟩$$
10	9	fveq2d	$$⊢s\in P\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)$$
11		id	$$⊢s\in P\to s\in P$$
12	9 11	eqeltrrd	$$⊢s\in P\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 P$$
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	6 1 2 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 P\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	12 14	syl	$$⊢s\in P\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	10 15	eqtrd	$$⊢s\in P\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		inss1	$$⊢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)\subseteq 1^{st}\left(1^{st}\left(s\right)\right)$$
18		eqid	$$⊢\mathrm{mDV}\left(T\right)=\mathrm{mDV}\left(T\right)$$
19		eqid	$$⊢\mathrm{mEx}\left(T\right)=\mathrm{mEx}\left(T\right)$$
20	18 19 1	elmpst	$$⊢⟨1^{st}\left(1^{st}\left(s\right)\right),2^{nd}\left(1^{st}\left(s\right)\right),2^{nd}\left(s\right)⟩\in P\leftrightarrow \left(\left(1^{st}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mDV}\left(T\right)\wedge {1^{st}\left(1^{st}\left(s\right)\right)}^{-1}=1^{st}\left(1^{st}\left(s\right)\right)\right)\wedge \left(2^{nd}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mEx}\left(T\right)\wedge 2^{nd}\left(1^{st}\left(s\right)\right)\in \mathrm{Fin}\right)\wedge 2^{nd}\left(s\right)\in \mathrm{mEx}\left(T\right)\right)$$
21	12 20	sylib	$$⊢s\in P\to \left(\left(1^{st}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mDV}\left(T\right)\wedge {1^{st}\left(1^{st}\left(s\right)\right)}^{-1}=1^{st}\left(1^{st}\left(s\right)\right)\right)\wedge \left(2^{nd}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mEx}\left(T\right)\wedge 2^{nd}\left(1^{st}\left(s\right)\right)\in \mathrm{Fin}\right)\wedge 2^{nd}\left(s\right)\in \mathrm{mEx}\left(T\right)\right)$$
22	21	simp1d	$$⊢s\in P\to \left(1^{st}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mDV}\left(T\right)\wedge {1^{st}\left(1^{st}\left(s\right)\right)}^{-1}=1^{st}\left(1^{st}\left(s\right)\right)\right)$$
23	22	simpld	$$⊢s\in P\to 1^{st}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mDV}\left(T\right)$$
24	17 23	sstrid	$$⊢s\in P\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)\subseteq \mathrm{mDV}\left(T\right)$$
25		cnvin	$$⊢{\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)}^{-1}={1^{st}\left(1^{st}\left(s\right)\right)}^{-1}\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}$$
26	22	simprd	$$⊢s\in P\to {1^{st}\left(1^{st}\left(s\right)\right)}^{-1}=1^{st}\left(1^{st}\left(s\right)\right)$$
27		cnvxp	$$⊢{\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}=\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]$$
28	27	a1i	$$⊢s\in P\to {\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}=\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]$$
29	26 28	ineq12d	$$⊢s\in P\to {1^{st}\left(1^{st}\left(s\right)\right)}^{-1}\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}=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)$$
30	25 29	syl5eq	$$⊢s\in P\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)}^{-1}=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)$$
31	24 30	jca	$$⊢s\in P\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)\subseteq \mathrm{mDV}\left(T\right)\wedge {\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)}^{-1}=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)$$
32	21	simp2d	$$⊢s\in P\to \left(2^{nd}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mEx}\left(T\right)\wedge 2^{nd}\left(1^{st}\left(s\right)\right)\in \mathrm{Fin}\right)$$
33	21	simp3d	$$⊢s\in P\to 2^{nd}\left(s\right)\in \mathrm{mEx}\left(T\right)$$
34	18 19 1	elmpst	$$⊢⟨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 P\leftrightarrow \left(\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)\subseteq \mathrm{mDV}\left(T\right)\wedge {\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)}^{-1}=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)\wedge \left(2^{nd}\left(1^{st}\left(s\right)\right)\subseteq \mathrm{mEx}\left(T\right)\wedge 2^{nd}\left(1^{st}\left(s\right)\right)\in \mathrm{Fin}\right)\wedge 2^{nd}\left(s\right)\in \mathrm{mEx}\left(T\right)\right)$$
35	31 32 33 34	syl3anbrc	$$⊢s\in P\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 P$$
36	16 35	eqeltrd	$$⊢s\in P\to R\left(s\right)\in P$$
37	36	rgen	$$⊢\forall s\in PR\left(s\right)\in P$$
38		ffnfv	$$⊢R:P⟶P\leftrightarrow \left(RFnP\wedge \forall s\in PR\left(s\right)\in P\right)$$
39	8 37 38	mpbir2an	$$⊢R:P⟶P$$