# Metamath Proof Explorer

## Theorem isgrpo

Description: The predicate "is a group operation." Note that X is the base set of the group. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis isgrp.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion isgrpo ${⊢}{G}\in {A}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 isgrp.1 ${⊢}{X}=\mathrm{ran}{G}$
2 feq1 ${⊢}{g}={G}\to \left({g}:{t}×{t}⟶{t}↔{G}:{t}×{t}⟶{t}\right)$
3 oveq ${⊢}{g}={G}\to \left({x}{g}{y}\right){g}{z}=\left({x}{g}{y}\right){G}{z}$
4 oveq ${⊢}{g}={G}\to {x}{g}{y}={x}{G}{y}$
5 4 oveq1d ${⊢}{g}={G}\to \left({x}{g}{y}\right){G}{z}=\left({x}{G}{y}\right){G}{z}$
6 3 5 eqtrd ${⊢}{g}={G}\to \left({x}{g}{y}\right){g}{z}=\left({x}{G}{y}\right){G}{z}$
7 oveq ${⊢}{g}={G}\to {x}{g}\left({y}{g}{z}\right)={x}{G}\left({y}{g}{z}\right)$
8 oveq ${⊢}{g}={G}\to {y}{g}{z}={y}{G}{z}$
9 8 oveq2d ${⊢}{g}={G}\to {x}{G}\left({y}{g}{z}\right)={x}{G}\left({y}{G}{z}\right)$
10 7 9 eqtrd ${⊢}{g}={G}\to {x}{g}\left({y}{g}{z}\right)={x}{G}\left({y}{G}{z}\right)$
11 6 10 eqeq12d ${⊢}{g}={G}\to \left(\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)↔\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
12 11 ralbidv ${⊢}{g}={G}\to \left(\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)↔\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
13 12 2ralbidv ${⊢}{g}={G}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)↔\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
14 oveq ${⊢}{g}={G}\to {u}{g}{x}={u}{G}{x}$
15 14 eqeq1d ${⊢}{g}={G}\to \left({u}{g}{x}={x}↔{u}{G}{x}={x}\right)$
16 oveq ${⊢}{g}={G}\to {y}{g}{x}={y}{G}{x}$
17 16 eqeq1d ${⊢}{g}={G}\to \left({y}{g}{x}={u}↔{y}{G}{x}={u}\right)$
18 17 rexbidv ${⊢}{g}={G}\to \left(\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}↔\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)$
19 15 18 anbi12d ${⊢}{g}={G}\to \left(\left({u}{g}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}\right)↔\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
20 19 rexralbidv ${⊢}{g}={G}\to \left(\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{g}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}\right)↔\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
21 2 13 20 3anbi123d ${⊢}{g}={G}\to \left(\left({g}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{g}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}\right)\right)↔\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
22 21 exbidv ${⊢}{g}={G}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({g}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{g}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}\right)\right)↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
23 df-grpo ${⊢}\mathrm{GrpOp}=\left\{{g}|\exists {t}\phantom{\rule{.4em}{0ex}}\left({g}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{g}{y}\right){g}{z}={x}{g}\left({y}{g}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{g}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{g}{x}={u}\right)\right)\right\}$
24 22 23 elab2g ${⊢}{G}\in {A}\to \left({G}\in \mathrm{GrpOp}↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
25 simpl ${⊢}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\to {u}{G}{x}={x}$
26 25 ralimi ${⊢}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\to \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}$
27 oveq2 ${⊢}{x}={z}\to {u}{G}{x}={u}{G}{z}$
28 id ${⊢}{x}={z}\to {x}={z}$
29 27 28 eqeq12d ${⊢}{x}={z}\to \left({u}{G}{x}={x}↔{u}{G}{z}={z}\right)$
30 eqcom ${⊢}{u}{G}{z}={z}↔{z}={u}{G}{z}$
31 29 30 syl6bb ${⊢}{x}={z}\to \left({u}{G}{x}={x}↔{z}={u}{G}{z}\right)$
32 31 rspcv ${⊢}{z}\in {t}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\to {z}={u}{G}{z}\right)$
33 oveq2 ${⊢}{y}={z}\to {u}{G}{y}={u}{G}{z}$
34 33 rspceeqv ${⊢}\left({z}\in {t}\wedge {z}={u}{G}{z}\right)\to \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}$
35 34 ex ${⊢}{z}\in {t}\to \left({z}={u}{G}{z}\to \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
36 32 35 syld ${⊢}{z}\in {t}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\to \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
37 26 36 syl5 ${⊢}{z}\in {t}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\to \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
38 37 reximdv ${⊢}{z}\in {t}\to \left(\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\to \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
39 38 impcom ${⊢}\left(\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\wedge {z}\in {t}\right)\to \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}$
40 39 ralrimiva ${⊢}\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\to \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}$
41 40 anim2i ${⊢}\left({G}:{t}×{t}⟶{t}\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\to \left({G}:{t}×{t}⟶{t}\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
42 foov ${⊢}{G}:{t}×{t}\underset{onto}{⟶}{t}↔\left({G}:{t}×{t}⟶{t}\wedge \forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{z}={u}{G}{y}\right)$
43 41 42 sylibr ${⊢}\left({G}:{t}×{t}⟶{t}\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\to {G}:{t}×{t}\underset{onto}{⟶}{t}$
44 forn ${⊢}{G}:{t}×{t}\underset{onto}{⟶}{t}\to \mathrm{ran}{G}={t}$
45 44 eqcomd ${⊢}{G}:{t}×{t}\underset{onto}{⟶}{t}\to {t}=\mathrm{ran}{G}$
46 43 45 syl ${⊢}\left({G}:{t}×{t}⟶{t}\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\to {t}=\mathrm{ran}{G}$
47 46 3adant2 ${⊢}\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\to {t}=\mathrm{ran}{G}$
48 47 pm4.71ri ${⊢}\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)↔\left({t}=\mathrm{ran}{G}\wedge \left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
49 48 exbii ${⊢}\exists {t}\phantom{\rule{.4em}{0ex}}\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{ran}{G}\wedge \left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
50 24 49 syl6bb ${⊢}{G}\in {A}\to \left({G}\in \mathrm{GrpOp}↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{ran}{G}\wedge \left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)\right)$
51 rnexg ${⊢}{G}\in {A}\to \mathrm{ran}{G}\in \mathrm{V}$
52 1 eqeq2i ${⊢}{t}={X}↔{t}=\mathrm{ran}{G}$
53 xpeq1 ${⊢}{t}={X}\to {t}×{t}={X}×{t}$
54 xpeq2 ${⊢}{t}={X}\to {X}×{t}={X}×{X}$
55 53 54 eqtrd ${⊢}{t}={X}\to {t}×{t}={X}×{X}$
56 55 feq2d ${⊢}{t}={X}\to \left({G}:{t}×{t}⟶{t}↔{G}:{X}×{X}⟶{t}\right)$
57 feq3 ${⊢}{t}={X}\to \left({G}:{X}×{X}⟶{t}↔{G}:{X}×{X}⟶{X}\right)$
58 56 57 bitrd ${⊢}{t}={X}\to \left({G}:{t}×{t}⟶{t}↔{G}:{X}×{X}⟶{X}\right)$
59 raleq ${⊢}{t}={X}\to \left(\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
60 59 raleqbi1dv ${⊢}{t}={X}\to \left(\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
61 60 raleqbi1dv ${⊢}{t}={X}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
62 rexeq ${⊢}{t}={X}\to \left(\exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)$
63 62 anbi2d ${⊢}{t}={X}\to \left(\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)↔\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
64 63 raleqbi1dv ${⊢}{t}={X}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
65 64 rexeqbi1dv ${⊢}{t}={X}\to \left(\exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)↔\exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)$
66 58 61 65 3anbi123d ${⊢}{t}={X}\to \left(\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
67 52 66 sylbir ${⊢}{t}=\mathrm{ran}{G}\to \left(\left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
68 67 ceqsexgv ${⊢}\mathrm{ran}{G}\in \mathrm{V}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{ran}{G}\wedge \left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
69 51 68 syl ${⊢}{G}\in {A}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{ran}{G}\wedge \left({G}:{t}×{t}⟶{t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}\forall {z}\in {t}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {t}\phantom{\rule{.4em}{0ex}}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {t}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$
70 50 69 bitrd ${⊢}{G}\in {A}\to \left({G}\in \mathrm{GrpOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{y}{G}{x}={u}\right)\right)\right)$