Definition df-mpst 31390

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

Assertion

Ref	Expression
df-mpst	|- mPreSt = ( t e. _V |-> ( ( { d e. ~P (mDV ` t ) | `' d = d } X. ( ~P (mEx ` t ) i^i Fin ) ) X. (mEx ` t ) ) )

Distinct variable group:   t, d

Detailed syntax breakdown of Definition df-mpst

Step	Hyp	Ref	Expression
1		cmpst 31370	. 2 class mPreSt
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vd	. . . . . . . . 9 setvar d
5	4	cv 1482	. . . . . . . 8 class d
6	5	ccnv 5113	. . . . . . 7 class `' d
7	6, 5	wceq 1483	. . . . . 6 wff `' d = d
8	2	cv 1482	. . . . . . . 8 class t
9		cmdv 31365	. . . . . . . 8 class mDV
10	8, 9	cfv 5888	. . . . . . 7 class (mDV ` t )
11	10	cpw 4158	. . . . . 6 class ~P (mDV ` t )
12	7, 4, 11	crab 2916	. . . . 5 class { d e. ~P (mDV ` t ) | `' d = d }
13		cmex 31364	. . . . . . . 8 class mEx
14	8, 13	cfv 5888	. . . . . . 7 class (mEx ` t )
15	14	cpw 4158	. . . . . 6 class ~P (mEx ` t )
16		cfn 7955	. . . . . 6 class Fin
17	15, 16	cin 3573	. . . . 5 class ( ~P (mEx ` t ) i^i Fin )
18	12, 17	cxp 5112	. . . 4 class ( { d e. ~P (mDV ` t ) | `' d = d } X. ( ~P (mEx ` t ) i^i Fin ) )
19	18, 14	cxp 5112	. . 3 class ( ( { d e. ~P (mDV ` t ) | `' d = d } X. ( ~P (mEx ` t ) i^i Fin ) ) X. (mEx ` t ) )
20	2, 3, 19	cmpt 4729	. 2 class ( t e. _V |-> ( ( { d e. ~P (mDV ` t ) | `' d = d } X. ( ~P (mEx ` t ) i^i Fin ) ) X. (mEx ` t ) ) )
21	1, 20	wceq 1483	1 wff mPreSt = ( t e. _V |-> ( ( { d e. ~P (mDV ` t ) | `' d = d } X. ( ~P (mEx ` t ) i^i Fin ) ) X. (mEx ` t ) ) )

This definition is referenced by:  mpstval  31432