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 = ( mStRed ` T )
	mthmval.j	|- J = ( mPPSt ` T )
	mthmval.u	|- U = ( mThm ` T )
Assertion	mthmval	|- U = ( `' R " ( R " J ) )

Proof

Step	Hyp	Ref	Expression
1		mthmval.r	|- R = ( mStRed ` T )
2		mthmval.j	|- J = ( mPPSt ` T )
3		mthmval.u	|- U = ( mThm ` T )
4		fveq2	|- ( t = T -> ( mStRed ` t ) = ( mStRed ` T ) )
5	4 1	eqtr4di	|- ( t = T -> ( mStRed ` t ) = R )
6	5	cnveqd	|- ( t = T -> `' ( mStRed ` t ) = `' R )
7		fveq2	|- ( t = T -> ( mPPSt ` t ) = ( mPPSt ` T ) )
8	7 2	eqtr4di	|- ( t = T -> ( mPPSt ` t ) = J )
9	5 8	imaeq12d	|- ( t = T -> ( ( mStRed ` t ) " ( mPPSt ` t ) ) = ( R " J ) )
10	6 9	imaeq12d	|- ( t = T -> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) = ( `' R " ( R " J ) ) )
11		df-mthm	|- mThm = ( t e. _V |-> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) )
12		fvex	|- ( mStRed ` t ) e. _V
13	12	cnvex	|- `' ( mStRed ` t ) e. _V
14		imaexg	|- ( `' ( mStRed ` t ) e. _V -> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) e. _V )
15	13 14	ax-mp	|- ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) e. _V
16	10 11 15	fvmpt3i	|- ( T e. _V -> ( mThm ` T ) = ( `' R " ( R " J ) ) )
17		0ima	|- ( (/) " ( R " J ) ) = (/)
18	17	eqcomi	|- (/) = ( (/) " ( R " J ) )
19		fvprc	|- ( -. T e. _V -> ( mThm ` T ) = (/) )
20		fvprc	|- ( -. T e. _V -> ( mStRed ` T ) = (/) )
21	1 20	syl5eq	|- ( -. T e. _V -> R = (/) )
22	21	cnveqd	|- ( -. T e. _V -> `' R = `' (/) )
23		cnv0	|- `' (/) = (/)
24	22 23	eqtrdi	|- ( -. T e. _V -> `' R = (/) )
25	24	imaeq1d	|- ( -. T e. _V -> ( `' R " ( R " J ) ) = ( (/) " ( R " J ) ) )
26	18 19 25	3eqtr4a	|- ( -. T e. _V -> ( mThm ` T ) = ( `' R " ( R " J ) ) )
27	16 26	pm2.61i	|- ( mThm ` T ) = ( `' R " ( R " J ) )
28	3 27	eqtri	|- U = ( `' R " ( R " J ) )