df-mid

		Ref	Expression
	Assertion	df-mid	$⊢ {mid}_{𝒢} = (g \in V ⟼ (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))))$

Step	Hyp	Ref	Expression
0		cmid	$class {mid}_{𝒢}$
1		vg	$setvar g$
2		cvv	$class V$
3		va	$setvar a$
4		cbs	$class Base$
5	1	cv	$setvar g$
6	5 4	cfv	$class {Base}_{g}$
7		vb	$setvar b$
8		vm	$setvar m$
9	7	cv	$setvar b$
10		cmir	$class {pInv}_{𝒢}$
11	5 10	cfv	$class {pInv}_{𝒢} (g)$
12	8	cv	$setvar m$
13	12 11	cfv	$class {pInv}_{𝒢} (g) (m)$
14	3	cv	$setvar a$
15	14 13	cfv	$class {pInv}_{𝒢} (g) (m) (a)$
16	9 15	wceq	$wff b = {pInv}_{𝒢} (g) (m) (a)$
17	16 8 6	crio	$class (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))$
18	3 7 6 6 17	cmpo	$class (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a)))$
19	1 2 18	cmpt	$class (g \in V ⟼ (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))))$
20	0 19	wceq	$wff {mid}_{𝒢} = (g \in V ⟼ (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))))$

Metamath Proof Explorer