Theorem mthmval

Description: A theorem is a pre-statement, whose reduct is also the reduct of a provable pre-statement. Unlike the difference between pre-statement and statement, this application of the reduct is not necessarily trivial: there are theorems that are not themselves provable but are provable once enough "dummy variables" are introduced. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mthmval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
	mthmval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
	mthmval.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
Assertion	mthmval	$$⊢U=R^{-1}\left[R\left[J\right]\right]$$

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mthmval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
3		mthmval.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
4		fveq2	$$⊢t=T\to \mathrm{mStRed}\left(t\right)=\mathrm{mStRed}\left(T\right)$$
5	4 1	eqtr4di	$$⊢t=T\to \mathrm{mStRed}\left(t\right)=R$$
6	5	cnveqd	$$⊢t=T\to {\mathrm{mStRed}\left(t\right)}^{-1}=R^{-1}$$
7		fveq2	$$⊢t=T\to \mathrm{mPPSt}\left(t\right)=\mathrm{mPPSt}\left(T\right)$$
8	7 2	eqtr4di	$$⊢t=T\to \mathrm{mPPSt}\left(t\right)=J$$
9	5 8	imaeq12d	$$⊢t=T\to \mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]=R\left[J\right]$$
10	6 9	imaeq12d	$$⊢t=T\to {\mathrm{mStRed}\left(t\right)}^{-1}\left[\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]\right]=R^{-1}\left[R\left[J\right]\right]$$
11		df-mthm	$$⊢\mathrm{mThm}=\left(t\in \mathrm{V}⟼{\mathrm{mStRed}\left(t\right)}^{-1}\left[\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]\right]\right)$$
12		fvex	$$⊢\mathrm{mStRed}\left(t\right)\in \mathrm{V}$$
13	12	cnvex	$$⊢{\mathrm{mStRed}\left(t\right)}^{-1}\in \mathrm{V}$$
14		imaexg	$$⊢{\mathrm{mStRed}\left(t\right)}^{-1}\in \mathrm{V}\to {\mathrm{mStRed}\left(t\right)}^{-1}\left[\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]\right]\in \mathrm{V}$$
15	13 14	ax-mp	$$⊢{\mathrm{mStRed}\left(t\right)}^{-1}\left[\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]\right]\in \mathrm{V}$$
16	10 11 15	fvmpt3i	$$⊢T\in \mathrm{V}\to \mathrm{mThm}\left(T\right)=R^{-1}\left[R\left[J\right]\right]$$
17		0ima	$$⊢\varnothing \left[R\left[J\right]\right]=\varnothing$$
18	17	eqcomi	$$⊢\varnothing =\varnothing \left[R\left[J\right]\right]$$
19		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mThm}\left(T\right)=\varnothing$$
20		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStRed}\left(T\right)=\varnothing$$
21	1 20	syl5eq	$$⊢\neg T\in \mathrm{V}\to R=\varnothing$$
22	21	cnveqd	$$⊢\neg T\in \mathrm{V}\to R^{-1}={\varnothing }^{-1}$$
23		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
24	22 23	eqtrdi	$$⊢\neg T\in \mathrm{V}\to R^{-1}=\varnothing$$
25	24	imaeq1d	$$⊢\neg T\in \mathrm{V}\to R^{-1}\left[R\left[J\right]\right]=\varnothing \left[R\left[J\right]\right]$$
26	18 19 25	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mThm}\left(T\right)=R^{-1}\left[R\left[J\right]\right]$$
27	16 26	pm2.61i	$$⊢\mathrm{mThm}\left(T\right)=R^{-1}\left[R\left[J\right]\right]$$
28	3 27	eqtri	$$⊢U=R^{-1}\left[R\left[J\right]\right]$$