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

A description of the preimage. Write $\breve{u}$ for the inverse relation of $u$, the class written $u^{-1}$ in Relations, Domain, Range, Inverse and Composition (iv). Let $V$ be a set. By The Image and the Preimage of a Class under a Class (ii) and The Image and the Preimage of a Class under a Class (i), $u^{-1}(V)$ is the image $\breve{u}[V]$, the class $\{v:\exists w\,(w\in V\wedge(w,v)\in\breve{u})\}$. For sets $w$ and $v$, by Relations, Domain, Range, Inverse and Composition (iv), $(w,v)\in\breve{u}$ if and only if there are sets $a$ and $b$ with $(a,b)\in u$ and $(w,v)=(b,a)$; by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i) the latter means $b=w$ and $a=v$. Hence $(w,v)\in\breve{u}$ if and only if $(v,w)\in u$, and for every set $s$,

$$s\in u^{-1}(V)\iff\exists w\,(w\in V\wedge(s,w)\in u). \tag{1}$$

Proof of (i). The formula $(s,w)\in u$ is predicative by 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), and $\pi$ applies no quantifier to a class variable, so $\pi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); its quantifiers bind $s$ and $w$, so its free variables are $z$, $V$ and $u$. Let $V$ be a set. If $s\in u^{-1}(V)$, then by (1) there is $w$ with $(s,w)\in u$, so $s\in\operatorname{dom}u$ by Relations, Domain, Range, Inverse and Composition (ii), and $\operatorname{dom}u=S$ by Functions, Values of a Function, and Functions from One Class to Another (iii). So $u^{-1}(V)$ is a subclass of $S$, hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), and a subset of $S$. For every set $z$, by (1), $\pi(z,V)$ holds if and only if $z$ and $u^{-1}(V)$ have the same elements, that is, by Axiom of Extensionality for Classes, if and only if $z=u^{-1}(V)$. So exactly one set $z$ satisfies $\pi(z,V)$, namely $u^{-1}(V)$, and by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii) $u^{-1}(V)$ is a defined set symbol given by $\pi$, used properly at every set $V$.

Proof of (ii). Let $V\subseteq T$ and let $s$ be a set. If $s\in S$ and $u(s)\in V$, then $(s,u(s))\in u$, so $w=u(s)$ witnesses the right side of (1) and $s\in u^{-1}(V)$. Conversely, let $s\in u^{-1}(V)$, and by (1) let $w\in V$ with $(s,w)\in u$. Then $s\in S$ by (i), and $u(s)=w$, so $u(s)\in V$.

Proof of (iii). By (i), $u^{-1}(V)$ is a defined set symbol with the argument $V$, used properly at every set $V$. For $V\in\mathcal{P}(T)$, $u^{-1}(V)$ is a subset of $S$ by (i), so $u^{-1}(V)\in\mathcal{P}(S)$ by The Union Set and the Power Set of a Set (ii). By Maps and Relations Given by Formulas (i), with $\mathcal{P}(T)$ and $\mathcal{P}(S)$ for its $a$ and $b$ and the expression $u^{-1}(V)$, 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)$.

Proof of (iv). Let $g$ be the map of (iii), and let $(V_{k})$ be a sequence in $\mathcal{P}(T)$, that is, a map $V:\mathbb{N}\to\mathcal{P}(T)$ by Sequences (i). By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), the composite $W=g\circ V$ is a map $\mathbb{N}\to\mathcal{P}(S)$, a sequence in $\mathcal{P}(S)$, with $W_{k}=g(V_{k})=u^{-1}(V_{k})$ for every $k\in\mathbb{N}$. If $(W'_{k})$ is a sequence in $\mathcal{P}(S)$ with $W'_{k}=u^{-1}(V_{k})$ for every $k\in\mathbb{N}$, then $W'$ and $W$ are maps $\mathbb{N}\to\mathcal{P}(S)$ with the same values, so $W'=W$.

Proof of (v). Let $\mathcal{F}$ also denote a variable whose value is $\mathcal{F}$, and let $B$ and $z$ be distinct set variables, distinct from $u$ and $\mathcal{F}$, with $\pi(z,B)$ the formula of (i) with $B$ for $V$, its bound variables chosen other than $B$, $z$ and $\mathcal{F}$. The formula $\exists z\,(\pi(z,B)\wedge z\in\mathcal{F})$ applies no quantifier to a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). For every set $B$, exactly one set $z$ satisfies $\pi(z,B)$, namely $u^{-1}(B)$, by (i); so this formula holds if and only if $u^{-1}(B)\in\mathcal{F}$. Hence the class $\{B\in\mathcal{P}(T):u^{-1}(B)\in\mathcal{F}\}$ is the class $\{B\in\mathcal{P}(T):\exists z\,(\pi(z,B)\wedge z\in\mathcal{F})\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii), and by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) a set $B$ belongs to it if and only if $B\in\mathcal{P}(T)$ and $u^{-1}(B)\in\mathcal{F}$, that is, by The Union Set and the Power Set of a Set (ii), if and only if $B\subseteq T$ and $u^{-1}(B)\in\mathcal{F}$. Each of its elements lies in $\mathcal{P}(T)$, so it is a subclass of the set $\mathcal{P}(T)$ by Subclasses and Subsets (i), and hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), and a subset of $\mathcal{P}(T)$.