elementary set theory - Proof that $X subseteq Y$ if and only if $X cup Y = Y$

This exercise (2.1.49) was taken from An Infinite Descent into Pure Mathematics.

Question

Let $X, Y$ be sets. Prove that $X \subseteq Y$ if and only if $X \cup Y = Y$.

Proof

Towards a contradiction, assume $X \not \subseteq Y$ if and only if $X \cup Y = Y$.

For $X \not \subseteq Y$, then $X$ must be non-empty and contain a set of elements, $N$ such that $N$ is disjoint with $Y$. Therefore, assume $X = \{x : x \in Y \vee x \in N\}$.

For $X \cup Y = Y$, $N = \{\}$. This is a contradiction with the assumption that $N$ is inhabited. Therefore, the assumption $X \subseteq Y$ if and only if $X \cup Y = Y$ cannot be true. We have shown that $X \subseteq Y$ if and only if $X \cup Y = Y$. $\Box$

Is this proof rigorous enough, and are there any improvements that can be made?

Answer

To prove a statement of the form $A \iff B$, you need to show that both implications $A \implies B$ and $B \implies A$ hold. I will sketch both directions but leave a few details for you to fill in.

First let's prove $X \subseteq Y \implies X \cup Y = Y$.

To do this, we assume that $X \subseteq Y$, and we need to prove that $X \cup Y = Y$. To prove equality of two sets, we need to prove containment in both directions: namely $X \cup Y \subseteq Y$ and $Y \subseteq X \cup Y$.

To prove the first containment $X \cup Y \subseteq Y$, start with the assumption $X \subseteq Y$. This implies that $X \cup Y \subseteq Y \cup Y$ (why?), and of course $Y \cup Y = Y$, so we conclude that $X\cup Y \subseteq Y$ as desired.

The second containment $Y \subseteq X \cup Y$ is always true and doesn't even require the assumption that $X \subseteq Y$ (why?)

Now let's prove $X \cup Y = Y \implies X \subseteq Y$.

So, assume that $X \cup Y = Y$. The containment $X \subseteq X \cup Y$ always holds (why?). By the assumption, the RHS of this containment equals $Y$. Thus $X \subseteq Y$ as desired.