Proof of Rectangles, Sections and the Swap: Set Identities

Every identity is an equality of sets and is checked elementwise: a pair $(u,v)$ lies in a product $C\times D$ if and only if $u\in C$ and $v\in D$ (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)), every element of $X\times Y$ is such a pair, two pairs are equal exactly when their entries are (The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i)), and $s\in u^{-1}(V)$ if and only if $u(s)\in V$, for $s$ in the domain of $u$ (Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (ii)).

Proof of (i). A pair $(u,v)$ lies in both $A\times B$ and $A'\times B'$ exactly when $u\in A$, $u\in A'$, $v\in B$ and $v\in B'$, that is, when $(u,v)\in(A\cap A')\times(B\cap B')$. For $y'\in Y$ we have $(x,y')\in A\times B$ if and only if $x\in A$ and $y'\in B$ (Sections of Subsets and Functions on a Product (i)); so $(A\times B)_{x}=B$ if $x\in A$, and $(A\times B)_{x}=\emptyset$ if $x\notin A$. The section at $y$ is the same computation in the first entry.

Proof of (ii). For $y'\in Y$: $(x,y')\in(X\times Y)\setminus E$ if and only if $(x,y')\notin E$, that is, $y'\notin E_{x}$; $(x,y')\in\bigcup_{k}E_{k}$ if and only if $(x,y')\in E_{k}$ for some $k$, that is, $y'\in(E_{k})_{x}$ for some $k$; and $(x,y')\in E\cap E'$ if and only if $y'\in E_{x}$ and $y'\in E'_{x}$. If $E\cap E'=\emptyset$, then $E_{x}\cap E'_{x}=(E\cap E')_{x}=\emptyset_{x}=\emptyset$. Sections at $y$ are treated in the same way.

Proof of (iii). For $y'\in Y$, $y'\in i_{x}^{-1}(E)$ if and only if $(x,y')=i_{x}(y')\in E$, that is, $y'\in E_{x}$; likewise $x'\in(i^{y})^{-1}(E)$ if and only if $(x',y)\in E$, that is, $x'\in E^{y}$.

Proof of (iv). For $(y',x')\in Y\times X$: $(y',x')\in t^{-1}(A\times B)$ if and only if $(x',y')\in A\times B$, that is, $y'\in B$ and $x'\in A$, that is, $(y',x')\in B\times A$. For $x'\in X$, $x'\in(t^{-1}(E))_{y}$ if and only if $(y,x')\in t^{-1}(E)$, that is, $(x',y)\in E$, that is, $x'\in E^{y}$; and for $y'\in Y$, $y'\in(t^{-1}(E))^{x}$ if and only if $(y',x)\in t^{-1}(E)$, that is, $(x,y')\in E$, that is, $y'\in E_{x}$.