df-mpps

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

		Ref	Expression
	Assertion	df-mpps	$⊢ mPPSt = (t \in V ⟼ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\})$

Step	Hyp	Ref	Expression
0		cmpps	$class mPPSt$
1		vt	$setvar t$
2		cvv	$class V$
3		vd	$setvar d$
4		vh	$setvar h$
5		va	$setvar a$
6	3	cv	$setvar d$
7	4	cv	$setvar h$
8	5	cv	$setvar a$
9	6 7 8	cotp	$class ⟨d, h, a⟩$
10		cmpst	$class mPreSt$
11	1	cv	$setvar t$
12	11 10	cfv	$class mPreSt (t)$
13	9 12	wcel	$wff ⟨d, h, a⟩ \in mPreSt (t)$
14		cmcls	$class mCls$
15	11 14	cfv	$class mCls (t)$
16	6 7 15	co	$class (d mCls (t) h)$
17	8 16	wcel	$wff a \in (d mCls (t) h)$
18	13 17	wa	$wff (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))$
19	18 3 4 5	coprab	$class \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\}$
20	1 2 19	cmpt	$class (t \in V ⟼ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\})$
21	0 20	wceq	$wff mPPSt = (t \in V ⟼ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\})$

Metamath Proof Explorer