Definition df-mthm

Description: Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmthm	$$class\mathrm{mThm}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmsr	$$class\mathrm{mStRed}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mStRed}\left(t\right)$$
6	5	ccnv	$$class{\mathrm{mStRed}\left(t\right)}^{-1}$$
7		cmpps	$$class\mathrm{mPPSt}$$
8	4 7	cfv	$$class\mathrm{mPPSt}\left(t\right)$$
9	5 8	cima	$$class\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]$$
10	6 9	cima	$$class{\mathrm{mStRed}\left(t\right)}^{-1}\left[\mathrm{mStRed}\left(t\right)\left[\mathrm{mPPSt}\left(t\right)\right]\right]$$
11	1 2 10	cmpt	$$class\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	0 11	wceq	$$wff\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)$$