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 = ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgi	⊢ GId
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vu	⊢ 𝑢
4	1	cv	⊢ 𝑔
5	4	crn	⊢ ran 𝑔
6		vx	⊢ 𝑥
7	3	cv	⊢ 𝑢
8	6	cv	⊢ 𝑥
9	7 8 4	co	⊢ ( 𝑢 𝑔 𝑥 )
10	9 8	wceq	⊢ ( 𝑢 𝑔 𝑥 ) = 𝑥
11	8 7 4	co	⊢ ( 𝑥 𝑔 𝑢 )
12	11 8	wceq	⊢ ( 𝑥 𝑔 𝑢 ) = 𝑥
13	10 12	wa	⊢ ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 )
14	13 6 5	wral	⊢ ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 )
15	14 3 5	crio	⊢ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) )
16	1 2 15	cmpt	⊢ ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )
17	0 16	wceq	⊢ GId = ( 𝑔 ∈ V ↦ ( ℩ 𝑢 ∈ ran 𝑔 ∀ 𝑥 ∈ ran 𝑔 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑔 𝑢 ) = 𝑥 ) ) )