Metamath Proof Explorer

Theorem grpoideu

Description: The left identity element of a group is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by NM, 14-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 ⊢ 𝑋 = ran 𝐺
Assertion grpoideu ( 𝐺 ∈ GrpOp → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 1 grpoidinv ⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) )
3 simpll ⊢ ( ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ( 𝑢 𝐺 𝑧 ) = 𝑧 )
4 3 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 )
5 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑢 𝐺 𝑧 ) = ( 𝑢 𝐺 𝑥 ) )
6 id ⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
7 5 6 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ↔ ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
8 7 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
9 4 8 sylib ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
10 9 adantl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
11 9 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
12 simpr ⊢ ( ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) )
13 12 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑧 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) )
14 oveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 𝐺 𝑧 ) = ( 𝑦 𝐺 𝑤 ) )
15 14 eqeq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ↔ ( 𝑦 𝐺 𝑤 ) = 𝑢 ) )
16 oveq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝐺 𝑦 ) = ( 𝑤 𝐺 𝑦 ) )
17 16 eqeq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 𝐺 𝑦 ) = 𝑢 ↔ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) )
18 15 17 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ↔ ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) ) )
19 18 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) ) )
20 19 rspcva ⊢ ( ( 𝑤 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) )
21 20 adantll ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) )
22 13 21 sylan2 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) )
23 1 grpoidinvlem4 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑤 ) = 𝑢 ∧ ( 𝑤 𝐺 𝑦 ) = 𝑢 ) ) → ( 𝑤 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑤 ) )
24 22 23 syldan ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) → ( 𝑤 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑤 ) )
25 24 an32s ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑤 ) )
26 25 adantllr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑤 ) )
27 26 adantr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) ) → ( 𝑤 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑤 ) )
28 oveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝑤 𝐺 𝑥 ) = ( 𝑤 𝐺 𝑢 ) )
29 id ⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
30 28 29 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑤 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑤 𝐺 𝑢 ) = 𝑢 ) )
31 30 rspcva ⊢ ( ( 𝑢 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) → ( 𝑤 𝐺 𝑢 ) = 𝑢 )
32 31 adantll ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) → ( 𝑤 𝐺 𝑢 ) = 𝑢 )
33 32 ad2ant2rl ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) ) → ( 𝑤 𝐺 𝑢 ) = 𝑢 )
34 33 adantllr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) ) → ( 𝑤 𝐺 𝑢 ) = 𝑢 )
35 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑢 𝐺 𝑥 ) = ( 𝑢 𝐺 𝑤 ) )
36 id ⊢ ( 𝑥 = 𝑤 → 𝑥 = 𝑤 )
37 35 36 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑤 ) = 𝑤 ) )
38 37 rspcva ⊢ ( ( 𝑤 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) → ( 𝑢 𝐺 𝑤 ) = 𝑤 )
39 38 ad2ant2lr ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) ) → ( 𝑢 𝐺 𝑤 ) = 𝑤 )
40 27 34 39 3eqtr3d ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) ) → 𝑢 = 𝑤 )
41 40 ex ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) → 𝑢 = 𝑤 ) )
42 11 41 mpand ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) )
43 42 ralrimiva ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) → ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) )
44 10 43 jca ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) ∧ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) ) )
45 44 ex ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) ) ) )
46 45 reximdva ⊢ ( 𝐺 ∈ GrpOp → ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ( 𝑧 𝐺 𝑢 ) = 𝑧 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑧 ) = 𝑢 ∧ ( 𝑧 𝐺 𝑦 ) = 𝑢 ) ) → ∃ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) ) ) )
47 2 46 mpd ⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) ) )
48 oveq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 𝐺 𝑥 ) = ( 𝑤 𝐺 𝑥 ) )
49 48 eqeq1d ⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑤 𝐺 𝑥 ) = 𝑥 ) )
50 49 ralbidv ⊢ ( 𝑢 = 𝑤 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 ) )
51 50 reu8 ⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∃ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( 𝑤 𝐺 𝑥 ) = 𝑥 → 𝑢 = 𝑤 ) ) )
52 47 51 sylibr ⊢ ( 𝐺 ∈ GrpOp → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )