Definition df-mpps

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

	Ref	Expression
Assertion	df-mpps	⊢ mPPSt = ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpps	⊢ mPPSt
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		vh	⊢ ℎ
5		va	⊢ 𝑎
6	3	cv	⊢ 𝑑
7	4	cv	⊢ ℎ
8	5	cv	⊢ 𝑎
9	6 7 8	cotp	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩
10		cmpst	⊢ mPreSt
11	1	cv	⊢ 𝑡
12	11 10	cfv	⊢ ( mPreSt ‘ 𝑡 )
13	9 12	wcel	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 )
14		cmcls	⊢ mCls
15	11 14	cfv	⊢ ( mCls ‘ 𝑡 )
16	6 7 15	co	⊢ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ )
17	8 16	wcel	⊢ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ )
18	13 17	wa	⊢ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) )
19	18 3 4 5	coprab	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) }
20	1 2 19	cmpt	⊢ ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) } )
21	0 20	wceq	⊢ mPPSt = ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) } )