| Description: Define the subclass
relationship. Definition 5.9 of [TakeutiZaring]
p. 17. For example, {1, 2} ⊆ {1, 2, 3}
(ex-ss 31034). Note
that 𝐴 ⊆ 𝐴 (proved in ssid 3930). Contrast this relationship with
the relationship 𝐴 ⊊ 𝐵 (as will be defined in df-pss 4014). For an
alternative definition, not requiring a dummy variable, see dfss2 4094.
Other possible definitions are given by dfss3 3897, dfss4 4214, sspss 4029,
ssequn1 4184, ssequn2 4187, sseqin2 4120, and ssdif0 4313.
We prefer the label "ss" ("subset") for ⊆, despite the fact that
it applies to classes. It is much more common to refer to this as the
subset relation than subclass, especially since most of the time the
arguments are in fact sets (and for pragmatic reasons we don't want to
need to use different operations for sets). The way set.mm is set up,
many things are technically classes despite morally (and provably) being
sets, like 1 (cf. df-1 11212
and 1ex 11307) or ℝ ( cf. df-r 11214
and
reex 11295). This has to do with the fact that there
are no "set
expressions": classes are expressions but there are only set
variables
in set.mm (cf.
https://us.metamath.org/downloads/grammar-ambiguity.txt 11295). This is
why we use ⊆ both for subclass relations
and for subset relations
and call it "subset". (Contributed by NM, 8-Jan-2002.)
Revised from
the original definition dfss2 4094. (Revised by GG,
15-May-2025.) |
