Definition df-mthm

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

	Ref	Expression
Assertion	df-mthm	⊢ mThm = ( 𝑡 ∈ V ↦ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmthm	⊢ mThm
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmsr	⊢ mStRed
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mStRed ‘ 𝑡 )
6	5	ccnv	⊢ ◡ ( mStRed ‘ 𝑡 )
7		cmpps	⊢ mPPSt
8	4 7	cfv	⊢ ( mPPSt ‘ 𝑡 )
9	5 8	cima	⊢ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) )
10	6 9	cima	⊢ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) )
11	1 2 10	cmpt	⊢ ( 𝑡 ∈ V ↦ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) )
12	0 11	wceq	⊢ mThm = ( 𝑡 ∈ V ↦ ( ◡ ( mStRed ‘ 𝑡 ) “ ( ( mStRed ‘ 𝑡 ) “ ( mPPSt ‘ 𝑡 ) ) ) )