Mario and Jim already provided very good explanations. Let me send mine
anyway!
A group is made up of two things: a set, which we call its "Base",
together with an operation, which is the "+g".
We're using functions, so for a group g, Base(g) is the base set, and
+g(g) is the operation.
In
The specific question of what it means for two restricted quantifiers to
be next to each other is perhaps best answered by pointing to a simpler
example like https://us.metamath.org/mpeuni/r19.12.html - the ∀푦 ∈ 퐵
∃푥 ∈ 퐴 휑 there has the same syntax as ∀푎 ∈ (Base‘푔)∃푚 ∈
(Base‘푔)(푚(+g‘푔)푎) =
The ∀푎 ∈ (Base‘푔) expression, or in ascii syntax "A. a e. (Base`g)" is
the beginning of the restricted forall quantifier "A. x e. A ph" where you
have highlighted just the "A. x e. A" part. It is read "for all x in A,
..." and denotes that some property "ph" holds for every x such that x e. A
Please pardon me for this rather basic question.
I have read https://us.metamath.org/mpeuni/mmset.html, especially on the
sections "The Axioms", "The Theory of Classes". I have basic knowledge on
set theory and classical logic, so I understand all the black symbols in
prepositional and