Set-sized objects and definable-class schemas

Use the first-order language of The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations: all quantified objects are sets, and a definable class $\{x:\phi (x,p)\}$ abbreviates a formula with set parameters $p$. It is not a new set or a domain for unrestricted quantification. Work with the usual set axioms, in particular The Axiom of Power Set: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\forall }t(t\in z\to t\in x)\to z\in y)$ and The Axiom Schema of Separation: for each formula $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (z,\bar{p})))$, and the ordered pairs, products and functions of The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,b\}\}$, The Cartesian product $A\times B:=\{z\in \mathcal{P}(\mathcal{P}(A\cup B)):\mathrm{\exists }a\in A\mathrm{\exists }b\in Bz=(a,b)\}$ and A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain. The power-set axiom supplies a collecting set; Separation trims it to exactly $\mathcal{P}(X)=\{Y:Y\subseteq X\}$.

A small category has a set $O$ of objects, a set $A$ of arrows, source and target functions $s,t:A\to O$, an identity function $e:O\to A$, and a composition function on the set $\{(a,b)\in A\times A:s(a)=t(b)\}$, where $ab$ denotes $a\circ b$ and the laws are $s(e(x))=t(e(x))=x$, $s(ab)=s(b)$, $t(ab)=t(a)$, $e(t(a))a=a=ae(s(a))$, and $(ab)c=a(bc)$ whenever the displayed compositions are defined. It is locally small when each specified hom-collection is a set. A definable large category is a schema of formulas for its objects, arrows and operations, with those laws asserted as formulas; it is not a set of all objects or a category of all large categories. No Grothendieck universe is assumed.

All indexed families in the local bundle construction have a supplied set index $I$. If $U_i\subseteq M$ and $G$ is a set, their tagged disjoint union is the subset $D=\{(i,x,z)\in I\times M\times G:x\in U_i\}$, formed by Separation. Given a set equivalence relation $E\subseteq D\times D$, each class $[u{]}_E=\{v\in D:(u,v)\in E\}$ is a subset of $D$, and the quotient is the set

$$D\mathrm{/}E=\{C\in \mathcal{P}(D):\mathrm{\exists }u\in D\mathrm{\forall }v\in D(v\in C⟺(u,v)\in E)\}\mathrm{.}$$

Thus the quotient is obtained by Separation in $\mathcal{P}(D)$, without choosing representatives. Transition-map graphs and connection data are subsets of specified finite products and power sets, not arbitrary proper-class objects.

For the Cauchy-development coding application, fix a set manifold $\mathrm{\Sigma }$ and the tensor-bundle total spaces over $\mathrm{\Sigma }\times \mathbb{R}$. A code consists of an open set $D\subseteq \mathrm{\Sigma }\times \mathbb{R}$, graphs of a metric and a two-form on $D$ inside those fixed total spaces, a time orientation, and a fixed initial embedding. All of its coordinates belong to fixed products and power sets. Separation selects the tuples satisfying the specified smoothness, Lorentzian, field-equation and initial-data formulas. Hence these codes form a set. This size assertion does not prove field-equation existence, maximality or uniqueness, and makes no proper-class representative choice.