Proof of Existence and Uniqueness of the Block Matrix with Two Row Blocks and Two Column Blocks

Each result cited is universally quantified over the data in its own statement.

Notation. Let $N=m+n$ and $P=[N]$, so $N\in\mathbb{N}$ and $[m]\subseteq P$ by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §sum, and let $Q=P\setminus[m]$. Entries are values: for a matrix $K$ and indices $k,l$, $K_{kl}=K(k,l)=K((k,l))$, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries. By Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §shift, the map $\sigma:[n]\to Q$, $\sigma(j)=m+j$, is a bijection. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, its inverse is a bijective map $\rho:Q\to[n]$ with $\rho\circ\sigma=\mathrm{id}_{[n]}$; so, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\rho(m+j)=j$ for every $j\in[n]$. For $l\in P$ with $l\notin[m]$, $l\in Q$, so $\rho(l)$ is defined and lies in $[n]$.

For sets $U$ and $W$, let $\pi_{1}:U\times W\to U$ and $\pi_{2}:U\times W\to W$ be the projections of Projection, Evaluation and Currying Maps §projections, so that $\pi_{1}(u,w)=u$ and $\pi_{2}(u,w)=w$ for $u\in U$ and $w\in W$; below, $U\times W$ is one of $[m]\times P$, $[n]\times P$ and $P\times P$, as indicated, each a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. Every element $x$ of $U\times W$ is a pair $x=(u,w)$ with $u\in U$ and $w\in W$, by The Cartesian Product of Two Classes §product, and then $x=(\pi_{1}(x),\pi_{2}(x))$.

Applying maps by cases. In each step below we use Maps Defined by Cases §cases. Its property is $\pi_{r}(x)\in[m]$ for $r=1$ or $r=2$, which, for $x$ in the product in question, is expressed by the predicative formula $\exists z\,((x,z)\in\pi_{r}\wedge z\in[m])$, with $\pi_{r}$ and $[m]$ as parameters, as $x\in\operatorname{dom}\pi_{r}$ by Functions, Values of a Function, and Functions from One Class to Another §map. Its expressions are built from the values of the maps $\pi_{1}$, $\pi_{2}$, $\rho$, $A$, $B$, $C$, $D$ and of the maps $R$ and $S$ constructed below, and from ordered pairs; values of functions and ordered pairs are defined set symbols by Functions, Values of a Function, and Functions from One Class to Another §value and The Ordered Pair of Two Sets and Nested Tuples §pair, and a value $F(c)$ is used properly when $c\in\operatorname{dom}F$. Values of maps lie in their codomains, and pairs lie in products by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership.

Step 1: the upper rows. On $[m]\times P$, take the property $\pi_{2}(x)\in[m]$, the expression $t_{1}(x)=A(x)$ and the expression $t_{2}(x)=B((\pi_{1}(x),\rho(\pi_{2}(x))))$. If $\pi_{2}(x)\in[m]$, then $x=(\pi_{1}(x),\pi_{2}(x))\in[m]\times[m]=\operatorname{dom}A$, so $A(x)$ is used properly and lies in $\mathbb{R}$. If not, then $\pi_{2}(x)\in Q=\operatorname{dom}\rho$ and $\rho(\pi_{2}(x))\in[n]$, so $(\pi_{1}(x),\rho(\pi_{2}(x)))\in[m]\times[n]=\operatorname{dom}B$, and $t_{2}(x)$ is used properly and lies in $\mathbb{R}$. This gives a map $R:[m]\times P\to\mathbb{R}$ with $R(x)=t_{1}(x)$ when $\pi_{2}(x)\in[m]$ and $R(x)=t_{2}(x)$ otherwise. For $k,l\in[m]$ and $j\in[n]$: $R(k,l)=A(k,l)=A_{kl}$; and since $m+j\in Q$, so $m+j\notin[m]$, by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §shift, $R(k,m+j)=B((k,\rho(m+j)))=B_{kj}$.

Step 2: the lower rows. On $[n]\times P$, the same argument with $C$ and $D$ in place of $A$ and $B$, and $[n]$ in place of $[m]$ in the first factor, gives a map $S:[n]\times P\to\mathbb{R}$ with $S(x)=C(x)$ when $\pi_{2}(x)\in[m]$ and $S(x)=D((\pi_{1}(x),\rho(\pi_{2}(x))))$ otherwise; so $S(i,l)=C_{il}$ and $S(i,m+j)=D_{ij}$ for $i,j\in[n]$ and $l\in[m]$.

Step 3: the matrix. On $P\times P$, take the property $\pi_{1}(x)\in[m]$, the expression $t_{1}(x)=R(x)$ and the expression $t_{2}(x)=S((\rho(\pi_{1}(x)),\pi_{2}(x)))$. If $\pi_{1}(x)\in[m]$, then $x=(\pi_{1}(x),\pi_{2}(x))\in[m]\times P=\operatorname{dom}R$; if not, then $\pi_{1}(x)\in Q$ and $(\rho(\pi_{1}(x)),\pi_{2}(x))\in[n]\times P=\operatorname{dom}S$; in both cases the expression is used properly and lies in $\mathbb{R}$. This gives a map $M:P\times P\to\mathbb{R}$, which lies in $\mathcal{M}_{N}(\mathbb{R})$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members. For $k,l\in[m]$ and $i,j\in[n]$, using $m+i\notin[m]$ and $\rho(m+i)=i$:

$$M_{kl}=R(k,l)=A_{kl},\quad M_{k,\,m+j}=R(k,m+j)=B_{kj},\quad M_{m+i,\,l}=S(i,l)=C_{il},\quad M_{m+i,\,m+j}=S(i,m+j)=D_{ij}.$$

This proves existence.

Uniqueness. Let $M'\in\mathcal{M}_{N}(\mathbb{R})$ have the same four families of entries, and let $k,l\in P$. By Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] §cases, $k\in[m]$ or $k=m+i$ for some $i\in[n]$, and $l\in[m]$ or $l=m+j$ for some $j\in[n]$. In each of the four combinations, $M'_{kl}$ and $M_{kl}$ are both given by the same displayed family, so $M'_{kl}=M_{kl}$. Hence $M'=M$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §equality.