Metamath Proof Explorer

Theorem isgrpoi

Description: Properties that determine a group operation. Read N as N ( x ) . (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isgrpoi.1 ⊢ X ∈ V
isgrpoi.2 ⊢ G : X × X ⟶ X
isgrpoi.3 ⊢ x ∈ X ∧ y ∈ X ∧ z ∈ X → x G y G z = x G y G z
isgrpoi.4 ⊢ U ∈ X
isgrpoi.5 ⊢ x ∈ X → U G x = x
isgrpoi.6 ⊢ x ∈ X → N ∈ X
isgrpoi.7 ⊢ x ∈ X → N G x = U
Assertion isgrpoi ⊢ G ∈ GrpOp

Proof

Step Hyp Ref Expression
1 isgrpoi.1 ⊢ X ∈ V
2 isgrpoi.2 ⊢ G : X × X ⟶ X
3 isgrpoi.3 ⊢ x ∈ X ∧ y ∈ X ∧ z ∈ X → x G y G z = x G y G z
4 isgrpoi.4 ⊢ U ∈ X
5 isgrpoi.5 ⊢ x ∈ X → U G x = x
6 isgrpoi.6 ⊢ x ∈ X → N ∈ X
7 isgrpoi.7 ⊢ x ∈ X → N G x = U
8 3 rgen3 ⊢ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
9 oveq1 ⊢ y = N → y G x = N G x
10 9 eqeq1d ⊢ y = N → y G x = U ↔ N G x = U
11 10 rspcev ⊢ N ∈ X ∧ N G x = U → ∃ y ∈ X y G x = U
12 6 7 11 syl2anc ⊢ x ∈ X → ∃ y ∈ X y G x = U
13 5 12 jca ⊢ x ∈ X → U G x = x ∧ ∃ y ∈ X y G x = U
14 13 rgen ⊢ ∀ x ∈ X U G x = x ∧ ∃ y ∈ X y G x = U
15 oveq1 ⊢ u = U → u G x = U G x
16 15 eqeq1d ⊢ u = U → u G x = x ↔ U G x = x
17 eqeq2 ⊢ u = U → y G x = u ↔ y G x = U
18 17 rexbidv ⊢ u = U → ∃ y ∈ X y G x = u ↔ ∃ y ∈ X y G x = U
19 16 18 anbi12d ⊢ u = U → u G x = x ∧ ∃ y ∈ X y G x = u ↔ U G x = x ∧ ∃ y ∈ X y G x = U
20 19 ralbidv ⊢ u = U → ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u ↔ ∀ x ∈ X U G x = x ∧ ∃ y ∈ X y G x = U
21 20 rspcev ⊢ U ∈ X ∧ ∀ x ∈ X U G x = x ∧ ∃ y ∈ X y G x = U → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
22 4 14 21 mp2an ⊢ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
23 1 1 xpex ⊢ X × X ∈ V
24 fex ⊢ G : X × X ⟶ X ∧ X × X ∈ V → G ∈ V
25 2 23 24 mp2an ⊢ G ∈ V
26 5 eqcomd ⊢ x ∈ X → x = U G x
27 rspceov ⊢ U ∈ X ∧ x ∈ X ∧ x = U G x → ∃ y ∈ X ∃ z ∈ X x = y G z
28 4 27 mp3an1 ⊢ x ∈ X ∧ x = U G x → ∃ y ∈ X ∃ z ∈ X x = y G z
29 26 28 mpdan ⊢ x ∈ X → ∃ y ∈ X ∃ z ∈ X x = y G z
30 29 rgen ⊢ ∀ x ∈ X ∃ y ∈ X ∃ z ∈ X x = y G z
31 foov ⊢ G : X × X ⟶ onto X ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∃ y ∈ X ∃ z ∈ X x = y G z
32 2 30 31 mpbir2an ⊢ G : X × X ⟶ onto X
33 forn ⊢ G : X × X ⟶ onto X → ran ⁡ G = X
34 32 33 ax-mp ⊢ ran ⁡ G = X
35 34 eqcomi ⊢ X = ran ⁡ G
36 35 isgrpo ⊢ G ∈ V → G ∈ GrpOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
37 25 36 ax-mp ⊢ G ∈ GrpOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ ∃ y ∈ X y G x = u
38 2 8 22 37 mpbir3an ⊢ G ∈ GrpOp