Metamath Proof Explorer

Definition df-gid

Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-gid	$⊢ GId = (g \in V ⟼ (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgi	$class GId$
1		vg	$setvar g$
2		cvv	$class V$
3		vu	$setvar u$
4	1	cv	$setvar g$
5	4	crn	$class ran g$
6		vx	$setvar x$
7	3	cv	$setvar u$
8	6	cv	$setvar x$
9	7 8 4	co	$class (u g x)$
10	9 8	wceq	$wff u g x = x$
11	8 7 4	co	$class (x g u)$
12	11 8	wceq	$wff x g u = x$
13	10 12	wa	$wff (u g x = x \land x g u = x)$
14	13 6 5	wral	$wff \forall x \in ran g (u g x = x \land x g u = x)$
15	14 3 5	crio	$class (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x))$
16	1 2 15	cmpt	$class (g \in V ⟼ (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x)))$
17	0 16	wceq	$wff GId = (g \in V ⟼ (ι u \in ran g \| \forall x \in ran g (u g x = x \land x g u = x)))$