description/proof of that for set and set, power set of [former set minus latter set] is [power set of former set] elements minus latter set
Topics
About: set
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Note
- 4: Proof
Starting Context
- The reader knows a definition of power set of set.
- The reader knows a definition of set elements minus set.
- The reader admits the proposition that for any set, the union of the power set of the set is the set.
Target Context
- The reader will have a description and a proof of the proposition that for any set and any set, the power set of [the former set minus the latter set] is [the power set of the former set] elements minus the latter set.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(S'\): \(\in \{\text{ the sets }\}\)
\(S\): \(\in \{\text{ the sets }\}\)
//
Statements:
\(Pow (S' \setminus S) = Pow (S') \setminus_e S\)
//
2: Natural Language Description
For any set, \(S'\), and any set, \(S\), \(Pow (S' \setminus S) = Pow (S') \setminus_e S\).
3: Note
The "[ ]" marks in the title and Target Context are in order for removing the ambiguities: for example, 'Power Set of Former Set Minus Latter Set' is ambiguous whether it is "Power Set of [Former Set Minus Latter Set]" or '[Power Set of Former Set] Minus Latter Set'.
4: Proof
Whole Strategy: Step 1: see that each element of \(Pow (S' \setminus S)\) is contained in \(Pow (S') \setminus_e S\); Step 2: see that each element of \(Pow (S') \setminus_e S\) is contained in \(Pow (S' \setminus S)\); Step 3: conclude the proposition.
Step 1:
Let \(S'' \in Pow (S' \setminus S)\) be any.
That means that \(S''\) is a subset of \(S' \setminus S\). So, there is a formula, \(\phi\), such that \(S'' = \{p \in S' \setminus S \vert \phi (p)\}\).
\(Pow (S') \setminus_e S = \{p \in Pow (\cup Pow (S')) \vert \exists p' \in Pow (S') (p = p' \setminus S)\}\), by the definition of set elements minus set. As \(\cup Pow (S') = S'\), by the proposition that for any set, the union of the power set of the set is the set, \(Pow (S') \setminus_e S = \{p \in Pow S' \vert \exists p' \in Pow (S') (p = p' \setminus S)\}\).
\(S'' \in Pow S'\), because \(S'' = \{p \in S' \vert p \in S' \setminus S \land \phi (p)\}\), because for each \(p' \in S''\), \(p' \in S'\), \(p' \in S' \setminus S\), and \(\phi (p)\); for each \(p' \in \{p \in S' \vert p \in S' \setminus S \land \phi (p)\}\), \(p' \in S' \setminus S\) and \(\phi (p)\), which means that \(p' \in S''\). \(\exists p' \in Pow (S') (S'' = p' \setminus S)\), because \(p' = S''\) will do.
So, \(S'' \in Pow (S') \setminus_e S\). So, \(Pow (S' \setminus S) \subseteq Pow (S') \setminus_e S\).
Step 2:
Let \(S'' \in Pow (S') \setminus_e S\) be any.
Is \(S''\) a subset of \(S' \setminus S\)?
There is a \(p' \in Pow (S')\) such that \(S'' = p' \setminus S\). As \(p'\) is a subset of \(S'\), there is a formula, \(\phi\), such that \(p' = \{p \in S' \vert \phi (p)\}\). As \(S'' = p' \setminus S\), \(S'' = \{p \in S' \vert \phi (p) \land p \in S' \setminus S\}\). But that equals \(S'' = \{p \in S' \setminus S \vert \phi (p)\}\), because for each \(p'' \in \{p \in S' \vert \phi (p) \land p \in S' \setminus S\}\), \(p'' \in S' \setminus S\) and \(\phi (p)\); for each \(p'' \in \{p \in S' \setminus S \vert \phi (p)\}\), \(p'' \in S'\), \(\phi (p)\), and \(p'' \in S' \setminus S\).
So, \(S''\) is a subset of \(S' \setminus S\).
So, \(S'' \in Pow (S' \setminus S)\). So, \(Pow (S') \setminus_e S \subseteq Pow (S' \setminus S)\).
Step 3:
So, \(Pow (S' \setminus S) = Pow (S') \setminus_e S\).
