Exercise 4, § 1

This solution was written by hy3-free and judged by a machine. It is not Bourbaki's and it has not been checked by a person.

By Definition 1 of §1 (tag 03H5), the relation $X \subset \{x\}$ is equivalent to $(\forall z)((z \in X) \Rightarrow (z \in \{x\}))$. By Definition 2 of §1 (tag 03H6), the relation $z \in \{x\}$ is equivalent to $z = x$. Hence $X \subset \{x\}$ is equivalent to $(\forall z)(z \in X \Rightarrow z = x)$.

Assume first that $X \subset \{x\}$ holds, so that $(\forall z)(z \in X \Rightarrow z = x)$ is true. By the standard law of excluded middle, either $X = \emptyset$ or $X \neq \emptyset$. By Theorem 1 of §1 (tag 03H9), the relation $(\forall z)(z \notin X)$ is equivalent to $X = \emptyset$. If $X = \emptyset$, then the disjunct $X = \emptyset$ is satisfied. If $X \neq \emptyset$, then by Theorem 1 of §1 and the standard negation of a universal quantifier there exists an object $a$ such that $a \in X$. From $(\forall z)(z \in X \Rightarrow z = x)$ we obtain $a = x$, and therefore $x \in X$. To prove $X = \{x\}$ it remains, by the axiom of extent (A1 of §1), to establish $\{x\} \subset X$. Let $z$ be an element of $\{x\}$; by Definition 2 of §1 this means $z = x$, and since $x \in X$ we have $z \in X$. Thus $\{x\} \subset X$ by Definition 1 of §1. Together with the hypothesis $X \subset \{x\}$ this gives $X = \{x\}$ by A1. Hence in all cases $X = \{x\}$ or $X = \emptyset$.

Conversely, assume that $X = \{x\}$ or $X = \emptyset$. If $X = \{x\}$, then $X \subset \{x\}$ is identical with $\{x\} \subset \{x\}$, which is true by Proposition 1 of §1 (tag 03P9). If $X = \emptyset$, then by Theorem 1 of §1 we have $\emptyset \subset Y$ for every set $Y$; taking $Y = \{x\}$ yields $X \subset \{x\}$. Thus the disjunction implies $X \subset \{x\}$.

Therefore the relation $X \subset \{x\}$ is equivalent to $X = \{x\}$ or $X = \emptyset$.