Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ssr Structured version   Visualization version   GIF version

Definition df-ssr 34588
Description: Define the subsets class or the class of all subset relations. Similar to definitions of epsilon relation (df-eprel 5163) and identity relation (df-id 5158) classes. Subset relation class and Scott Fenton's subset class df-sset 32300 are the same: S = SSet (compare dfssr2 34589 with df-sset 32300, cf. comment of df-xrn 34473), the only reason we do not use dfssr2 34589 as the base definition of the subsets class is the way we defined the epsilon relation and the identity relation classes.

The binary relation on the class of all subsets and the subclass relationship (df-ss 3737) are the same, that is, (𝐴 S 𝐵𝐴𝐵) when 𝐵 is a set, cf. brssr 34591. Yet in general we use the subclass relation 𝐴𝐵 both for classes and for sets, cf. the comment of df-ss 3737. The only exception (aside from directly investigating the class S e.g. in relssr 34590 or in extssr 34599) is when we have a specific purpose with its usage, like in case of df-refs 34600 vs. df-cnvrefs 34613, where we need S to define the class of reflexive sets in order to be able to define the class of converse reflexive sets with the help of the converse of S.

The subsets class S has another place in set.mm as well: if we define extensional relation based on the common property in extid 34422, extep 34389 and extssr 34599, then "extrelssr" " |- ExtRel _S " is a theorem along with "extrelep" " |- ExtRel _E " and "extrelid" " |- ExtRel _I ". (Contributed by Peter Mazsa, 25-Jul-2019.)

Assertion
Ref Expression
df-ssr S = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ssr
StepHypRef Expression
1 cssr 34316 . 2 class S
2 vx . . . . 5 setvar 𝑥
32cv 1630 . . . 4 class 𝑥
4 vy . . . . 5 setvar 𝑦
54cv 1630 . . . 4 class 𝑦
63, 5wss 3723 . . 3 wff 𝑥𝑦
76, 2, 4copab 4847 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
81, 7wceq 1631 1 wff S = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
Colors of variables: wff setvar class
This definition is referenced by:  dfssr2  34589  relssr  34590  brssr  34591
  Copyright terms: Public domain W3C validator