Image under Inclusion Mapping

Theorem

Let $X$ be a set.

Let $S \subseteq X$, $Z \subseteq S$.

Then $i_S \sqbrk Z = Z$

where

$i_S$ denotes the inclusion mapping of $S$

$i_S \sqbrk Z$ denotes the image of $Z$ under $i_S$.

Proof

\(\ds i_S \sqbrk Z\)

\(=\)

\(\ds \set {\map {i_S} z: z \in Z}\)

Definition of Image of Subset under Mapping

\(\ds \)

\(=\)

\(\ds \set {z: z \in Z}\)

Definition of Inclusion Mapping

\(\ds \)

\(=\)

\(\ds Z\)

Definition of Set Equality

$\blacksquare$

Sources

• Mizar article COMPACT1:2