Proof of The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets

By Indexed Families of Sets and Their Union, Intersection and Product §family, $A$ is a function with $\operatorname{dom}A=I$ and $A_{i}=A(i)$ for $i\in I$. We use repeatedly the following consequence of Functions, Values of a Function, and Functions from One Class to Another §value: for $i\in I$ and every set $w$, $(i,w)\in A$ if and only if $w=A_{i}$. Indeed $A_{i}$ is the unique set $w$ with $(i,w)\in A$.

Union. Let $I$ be a set. By Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §image-set, the image $A[I]$ is a set, since $I$ is a set and $A$ is a function; hence its union set $\bigcup(A[I])$ is a set by The Union Set and the Power Set of a Set §union. Let $u$ be a set. By The Union Set and the Power Set of a Set §union, $u\in\bigcup(A[I])$ if and only if there is a set $w$ with $u\in w$ and $w\in A[I]$; by The Image and the Preimage of a Class under a Class §image, $w\in A[I]$ if and only if there is $i\in I$ with $(i,w)\in A$, that is, by the consequence above, with $w=A_{i}$. Hence $u\in\bigcup(A[I])$ if and only if there is $i\in I$ with $u\in A_{i}$, which by Indexed Families of Sets and Their Union, Intersection and Product §union holds if and only if $u\in\bigcup_{i\in I}A_{i}$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\bigcup_{i\in I}A_{i}=\bigcup(A[I])$, which is a set.

Intersection. Here $I$ is any class with an element; let $i_{0}\in I$. If $u\in\bigcap_{i\in I}A_{i}$, then by Indexed Families of Sets and Their Union, Intersection and Product §intersection $u\in A_{i}$ for every $i\in I$, in particular $u\in A_{i_{0}}$. So $\bigcap_{i\in I}A_{i}$ is a subclass of the set $A_{i_{0}}$, and it is 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 §subclass.

Product. Let $I$ be a set, and write $U=\bigcup_{i\in I}A_{i}$, a set by the Union part above. Let $f\in\prod_{i\in I}A_{i}$. By Indexed Families of Sets and Their Union, Intersection and Product §product, $f$ is a function with $\operatorname{dom}f=I$ and $f(i)\in A_{i}$ for every $i\in I$. Let $v\in\operatorname{ran}f$. By Relations, Domain, Range, Inverse and Composition §range there is a set $i$ with $(i,v)\in f$; then $i\in\operatorname{dom}f=I$ by Relations, Domain, Range, Inverse and Composition §domain, and $v=f(i)$ by Functions, Values of a Function, and Functions from One Class to Another §value. Hence $v\in A_{i}$ with $i\in I$, so $v\in U$ by Indexed Families of Sets and Their Union, Intersection and Product §union. Thus $\operatorname{ran}f\subseteq U$, and $f$ is a function from $I$ to $U$ by Functions, Values of a Function, and Functions from One Class to Another §map; that is, $f$ is an element of the set of functions $U^{I}$ of The Class of All Functions from One Set to Another §functions. So $\prod_{i\in I}A_{i}$ is a subclass of $U^{I}$, which is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §set because $I$ and $U$ are sets. 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 §subclass, $\prod_{i\in I}A_{i}$ is a set.