Definition df-gid 30513

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.)

Assertion

Ref	Expression
df-gid	⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))

Distinct variable group:   𝑢,𝑔,𝑥

Detailed syntax breakdown of Definition df-gid

Step	Hyp	Ref	Expression
1		cgi 30509	. 2 class GId
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vu	. . . . . . . . 9 setvar 𝑢
5	4	cv 1539	. . . . . . . 8 class 𝑢
6		vx	. . . . . . . . 9 setvar 𝑥
7	6	cv 1539	. . . . . . . 8 class 𝑥
8	2	cv 1539	. . . . . . . 8 class 𝑔
9	5, 7, 8	co 7431	. . . . . . 7 class (𝑢𝑔𝑥)
10	9, 7	wceq 1540	. . . . . 6 wff (𝑢𝑔𝑥) = 𝑥
11	7, 5, 8	co 7431	. . . . . . 7 class (𝑥𝑔𝑢)
12	11, 7	wceq 1540	. . . . . 6 wff (𝑥𝑔𝑢) = 𝑥
13	10, 12	wa 395	. . . . 5 wff ((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)
14	8	crn 5686	. . . . 5 class ran 𝑔
15	13, 6, 14	wral 3061	. . . 4 wff ∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)
16	15, 4, 14	crio 7387	. . 3 class (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥))
17	2, 3, 16	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
18	1, 17	wceq 1540	1 wff GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))

This definition is referenced by:  gidval  30531