df-mpst

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

		Ref	Expression
	Assertion	df-mpst	$⊢ mPreSt = (t \in V ⟼ (\{d \in 𝒫 mDV (t) \| d^{-1} = d\} \times (𝒫 mEx (t) \cap Fin)) \times mEx (t))$

Step	Hyp	Ref	Expression
0		cmpst	$class mPreSt$
1		vt	$setvar t$
2		cvv	$class V$
3		vd	$setvar d$
4		cmdv	$class mDV$
5	1	cv	$setvar t$
6	5 4	cfv	$class mDV (t)$
7	6	cpw	$class 𝒫 mDV (t)$
8	3	cv	$setvar d$
9	8	ccnv	$class d^{-1}$
10	9 8	wceq	$wff d^{-1} = d$
11	10 3 7	crab	$class \{d \in 𝒫 mDV (t) \| d^{-1} = d\}$
12		cmex	$class mEx$
13	5 12	cfv	$class mEx (t)$
14	13	cpw	$class 𝒫 mEx (t)$
15		cfn	$class Fin$
16	14 15	cin	$class (𝒫 mEx (t) \cap Fin)$
17	11 16	cxp	$class (\{d \in 𝒫 mDV (t) \| d^{-1} = d\} \times (𝒫 mEx (t) \cap Fin))$
18	17 13	cxp	$class ((\{d \in 𝒫 mDV (t) \| d^{-1} = d\} \times (𝒫 mEx (t) \cap Fin)) \times mEx (t))$
19	1 2 18	cmpt	$class (t \in V ⟼ (\{d \in 𝒫 mDV (t) \| d^{-1} = d\} \times (𝒫 mEx (t) \cap Fin)) \times mEx (t))$
20	0 19	wceq	$wff mPreSt = (t \in V ⟼ (\{d \in 𝒫 mDV (t) \| d^{-1} = d\} \times (𝒫 mEx (t) \cap Fin)) \times mEx (t))$

Metamath Proof Explorer