We have the assertion: copab $a class { < x , y > | ph } $.
My question is how does one know that < x , y > refers to: cop $a class < A
, B > $.
Couldn't the "<" and ">" be just notational constants to syntactically form
the class expression being introduced?
In particular, just like the introduction of new wffs, shouldn't we have a
detailed syntax breakdown of this "axiom" ?
Something like the following:
-- Detailed syntax breakdown --
wph ph
vx setvar x
cv class x
vy setvar y
cv class y
cop class < x , y >
class using constants { | } and wff and a particular type of class
depending on x and y
Of course, that last line is the fuzzy one (whereas detailed syntax
breakdown for wffs doesn't have that fuzziness)
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/756d03e6-0ed6-43bc-89b8-0525a897caffn%40googlegroups.com.
