Theorem gidval 30661

Description: The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

Hypothesis

Ref	Expression
gidval.1	⊢ 𝑋 = ran 𝐺

Assertion

Ref	Expression
gidval	⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))

Distinct variable groups:   𝑥,𝑢,𝐺   𝑢,𝑋,𝑥

Allowed substitution hints:   𝑉(𝑥,𝑢)

Proof of Theorem gidval

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3474	. 2 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
2		rneq 5910	. . . . 5 ⊢ (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
3		gidval.1	. . . . 5 ⊢ 𝑋 = ran 𝐺
4	2, 3	eqtr4di 2814	. . . 4 ⊢ (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
5		oveq 7398	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑢𝑔𝑥) = (𝑢𝐺𝑥))
6	5	eqeq1d 2763	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑢𝑔𝑥) = 𝑥 ↔ (𝑢𝐺𝑥) = 𝑥))
7		oveq 7398	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑥𝑔𝑢) = (𝑥𝐺𝑢))
8	7	eqeq1d 2763	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑥𝑔𝑢) = 𝑥 ↔ (𝑥𝐺𝑢) = 𝑥))
9	6, 8	anbi12d 641	. . . . 5 ⊢ (𝑔 = 𝐺 → (((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥) ↔ ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
10	4, 9	raleqbidv 3335	. . . 4 ⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥) ↔ ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
11	4, 10	riotaeqbidv 7352	. . 3 ⊢ (𝑔 = 𝐺 → (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
12		df-gid 30643	. . 3 ⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))
13		riotaex 7353	. . 3 ⊢ (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)) ∈ V
14	11, 12, 13	fvmpt 6971	. 2 ⊢ (𝐺 ∈ V → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
15	1, 14	syl 17	1 ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  Vcvv 3453  ran crn 5646  ‘cfv 6517  ℩crio 7348  (class class class)co 7392  GIdcgi 30639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-riota 7349  df-ov 7395  df-gid 30643

This theorem is referenced by:  grpoidval  30662  idrval  38320  exidresid  38342