Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $S$ and $T$ be sets and let $u:S\to T$ be a map. Let $\mathcal{P}(S)$ and $\mathcal{P}(T)$ be the power sets of $S$ and $T$. For every set $V$, $u^{-1}(V)$ denotes the preimage $u^{-1}[V]$ of $V$ under $u$ of The Image and the Preimage of a Class under a Class (ii); for a subset $V$ of $T$ this is the preimage of Sets and Maps: Ordinary Notation (vii). Sequences are as in Sequences (i), and predicative is meant for formulas written with abbreviations.

(i) Let $z$, $V$, $s$ and $w$ be distinct set variables, and let $u$ also denote a variable of either kind, distinct from them, whose value is the map $u$. Let $\pi(z,V)$ be the formula

$$\forall s\,\bigl(s\in z\Leftrightarrow\exists w\,(w\in V\wedge(s,w)\in u)\bigr),$$

with $(s,w)\in u$ as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii). Then $\pi$ is predicative, its free variables are $z$, $V$ and $u$, and for all sets $V$ and $z$: $u^{-1}(V)$ is a set and a subset of $S$, and $\pi(z,V)$ holds if and only if $z=u^{-1}(V)$. Thus $u^{-1}(V)$ is a defined set symbol with the argument $V$ and the parameter $u$, given by $\pi$ and used properly at every set $V$.

(ii) For every subset $V$ of $T$ and every set $s$: $s\in u^{-1}(V)$ if and only if $s\in S$ and $u(s)\in V$.

(iii) There is exactly one map $g:\mathcal{P}(T)\to\mathcal{P}(S)$ with $g(V)=u^{-1}(V)$ for every $V\in\mathcal{P}(T)$.

(iv) Let $(V_{k})$ be a sequence in $\mathcal{P}(T)$. There is exactly one sequence $(W_{k})$ in $\mathcal{P}(S)$ with $W_{k}=u^{-1}(V_{k})$ for every $k\in\mathbb{N}$.

(v) Let $\mathcal{F}$ be a set. The class $\{B\in\mathcal{P}(T):u^{-1}(B)\in\mathcal{F}\}$ of those sets $B$ with $B\subseteq T$ and $u^{-1}(B)\in\mathcal{F}$ is a set and a subset of $\mathcal{P}(T)$; for every set $B$, $B$ belongs to it if and only if $B\subseteq T$ and $u^{-1}(B)\in\mathcal{F}$.