Definition df-mpps 34787

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

Assertion

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

Distinct variable group:   𝑎,𝑑,ℎ,𝑡

Detailed syntax breakdown of Definition df-mpps

Step	Hyp	Ref	Expression
1		cmpps 34767	. 2 class mPPSt
2		vt	. . 3 setvar 𝑡
3		cvv 3472	. . 3 class V
4		vd	. . . . . . . 8 setvar 𝑑
5	4	cv 1538	. . . . . . 7 class 𝑑
6		vh	. . . . . . . 8 setvar ℎ
7	6	cv 1538	. . . . . . 7 class ℎ
8		va	. . . . . . . 8 setvar 𝑎
9	8	cv 1538	. . . . . . 7 class 𝑎
10	5, 7, 9	cotp 4635	. . . . . 6 class ⟨𝑑, ℎ, 𝑎⟩
11	2	cv 1538	. . . . . . 7 class 𝑡
12		cmpst 34762	. . . . . . 7 class mPreSt
13	11, 12	cfv 6542	. . . . . 6 class (mPreSt‘𝑡)
14	10, 13	wcel 2104	. . . . 5 wff ⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡)
15		cmcls 34766	. . . . . . . 8 class mCls
16	11, 15	cfv 6542	. . . . . . 7 class (mCls‘𝑡)
17	5, 7, 16	co 7411	. . . . . 6 class (𝑑(mCls‘𝑡)ℎ)
18	9, 17	wcel 2104	. . . . 5 wff 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ)
19	14, 18	wa 394	. . . 4 wff (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))
20	19, 4, 6, 8	coprab 7412	. . 3 class {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))}
21	2, 3, 20	cmpt 5230	. 2 class (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})
22	1, 21	wceq 1539	1 wff mPPSt = (𝑡 ∈ V ↦ {⟨⟨𝑑, ℎ⟩, 𝑎⟩ ∣ (⟨𝑑, ℎ, 𝑎⟩ ∈ (mPreSt‘𝑡) ∧ 𝑎 ∈ (𝑑(mCls‘𝑡)ℎ))})

This definition is referenced by:  mppsval  34861