Metamath Proof Explorer

Definition df-mpst

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpst 
 |-  mPreSt
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vd 
 |-  d
4 cmdv 
 |-  mDV
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mDV ` t )
7 6 cpw 
 |-  ~P ( mDV ` t )
8 3 cv 
 |-  d
9 8 ccnv 
 |-  `' d
10 9 8 wceq 
 |-  `' d = d
11 10 3 7 crab 
 |-  { d e. ~P ( mDV ` t ) | `' d = d }
12 cmex 
 |-  mEx
13 5 12 cfv 
 |-  ( mEx ` t )
14 13 cpw 
 |-  ~P ( mEx ` t )
15 cfn 
 |-  Fin
16 14 15 cin 
 |-  ( ~P ( mEx ` t ) i^i Fin )
17 11 16 cxp 
 |-  ( { d e. ~P ( mDV ` t ) | `' d = d } X. ( ~P ( mEx ` t ) i^i Fin ) )
18 17 13 cxp 
 |-  ( ( { d e. ~P ( mDV ` t ) | `' d = d } X. ( ~P ( mEx ` t ) i^i Fin ) ) X. ( mEx ` t ) )
19 1 2 18 cmpt 
 |-  ( t e. _V |-> ( ( { d e. ~P ( mDV ` t ) | `' d = d } X. ( ~P ( mEx ` t ) i^i Fin ) ) X. ( mEx ` t ) ) )
20 0 19 wceq 
 |-  mPreSt = ( t e. _V |-> ( ( { d e. ~P ( mDV ` t ) | `' d = d } X. ( ~P ( mEx ` t ) i^i Fin ) ) X. ( mEx ` t ) ) )