Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union
Jump to navigation
Jump to search
Theorem
Let $S$ and $T$ be sets.
Let $S \times T$ be the Cartesian product of $S$ and $T$ realized as a set of ordered pairs in Kuratowski formalization.
Then $S \times T \subseteq \powerset {\powerset {S \cup T} }$.
Proof 1
Let $x \in S$ and $y \in T$.
We are to show that $\set {\set x, \set {x, y} } \in \powerset {\powerset {S \cup T} }$.
\(\ds x\) | \(\in\) | \(\ds S \cup T\) | Definition of Set Union | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set x\) | \(\in\) | \(\ds \powerset{S \cup T}\) | Definition of Power Set | ||||||||||
\(\ds y\) | \(\in\) | \(\ds S \cup T\) | Definition of Set Union | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set {x, y}\) | \(\in\) | \(\ds \powerset {S \cup T}\) | Definition of Power Set | ||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set {\set x, \set {x, y} }\) | \(\in\) | \(\ds \powerset {\powerset {S \cup T} }\) | Definition of Power Set |
$\blacksquare$
Proof 2
By Law of Excluded Middle there are two choices:
- $S \times T = \O$
- $S \times T \ne \O$
Suppose $S \times T = \O$.
By Empty Set is Subset of Power Set:
- $S \times T \subseteq \powerset {\powerset {S \cup T} }$
Suppose $S \times T \ne \O$.
By Cartesian Product is Empty iff Factor is Empty, there exist $x$ and $y$ such that:
- $x \in S$
- $y \in T$
Let us express the ordered pair $\tuple {x, y}$ using the Kuratowski formalization:
- $\tuple {x, y} \equiv \set { \set x, \set {x, y} }$
We now show that:
- $\set {\set x, \set {x, y} } \in \powerset {\powerset {S \cup T} }$
Indeed:
\(\ds x\) | \(\in\) | \(\ds S \cup T\) | Definition of Set Union | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set x\) | \(\in\) | \(\ds \powerset{S \cup T}\) | Definition of Power Set | ||||||||||
\(\ds y\) | \(\in\) | \(\ds S \cup T\) | Definition of Set Union | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set {x, y}\) | \(\in\) | \(\ds \powerset {S \cup T}\) | Definition of Power Set | ||||||||||
\(\ds \leadsto \ \ \) | \(\ds \set {\set x, \set {x, y} }\) | \(\in\) | \(\ds \powerset {\powerset {S \cup T} }\) | Definition of Power Set |
$\blacksquare$