Return to Answer

The short proofs of the following two lemmas were suggested by Pace Nielsen in his comments below.

Proof. Observe that $pr_1=dom[A]$ where $A=\{((x,y),((a,b),c)):x=((a,b),c),\;y=a\}$.

Write $A$ as $A=A_1\cap A_2$, where $A_1=\{((x,y),((a,b),c)):x=((a,b),c)\}$ and $A_2=\{((x,y),((a,b),c)):y=a\}$.

Observe that $\pi_3[A_1]=\{((((a,b),c),x),y):x=((a,b),c)\}=\{(((a,b),c),x):x=((a,b),c)\}\times V=((V^3\times V)\cap I)\times V$, which implies that $A_1$ exists. Here $V^3=((V\times V)\times V)$.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=a\}=\{(y,((a,b),c)):y=a\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=a\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=a\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=a\}=C\times V$ where $C=\{(y,(a,b)):y=a\}$. Observe that $\pi_2[C]=\{((a,b),y):y=a\}$ and $\pi_3[\pi_2[C]]=\{((y,a),b):y=a\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ exist and so does the class $pr_1=dom[A_1\cap A_2]$.  $\quad\square$

Proof. Observe that $pr_2=dom[A]$ where $A=\{((x,y),((a,b),c)):x=((a,b),c),\;y=b\}$.

Write $A$ as $A=A_1\cap A_2$, where $A_1=\{((x,y),((a,b),c)):x=((a,b),c)\}$ and $A_2=\{((x,y),((a,b),c)):y=b\}$. By analogy with Lemma 5 we can prove that the class $A_1$ exists.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=b\}=\{(y,((a,b),c)):y=b\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=b\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=b\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=b\}=C\times V$ where $C=\{(y,(a,b)):y=b\}$. Observe that $\pi_2[C]=\{((a,b),y):y=b\}$ and $\pi_3^2[\pi_2[C]]=\{((b,y),a):b=y\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ and finally $pr_2$ exist. $\quad\square$

Proof. Observe that $pr_3=dom[A]$ where $A=\{((x,y),((a,b),c)):x=((a,b),c),\;y=c\}$.

Write $A$ as $A=A_1\cap A_2$, where $A_1=\{((x,y),((a,b),c)):x=((a,b),c)\}$ and $A_2=\{((x,y),((a,b),c)):y=c\}$. By analogy with Lemma 5 we can prove that the class $A_1$ exists.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=c\}=\{(y,((a,b),c)):y=c\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=c\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=c\}$, $\pi^2_3[\pi_2[B]]=\{((c,y),(a,b)):c=y\}=I\times (V\times V)$. Then $A_2$ and exists and so does $pr_3$. $\quad\square$

The short proofs of the following five lemmas were suggested by Pace Nielsen in his comments below.

Proof. Observe that $\pi_3[pr_1]=\{((a,(a,b)),c):a,b,c\in V\}=\pi_2[p_1]\times V$ and hence the classes $\pi_3[pr_1]$ and $pr_1$ exist by Lemma 4 and Axioms of Inversion, Product, and Circular Permutation.  $\quad\square$

Proof. Observe that $\pi_3[pr_2]=\{((b,(a,b)),c):a,b,c\in V\}=\pi_2[p_2]\times V$ and hence the classes $\pi_3[pr_2]$ exist by Lemma 4 and Axioms of Inversion, Product, and Circular Permutation. $\quad\square$

Proof. Observe that $\pi^{-1}_3[pr_3]=\{((c,c),(a,b)):a,b,c\in V\}=I\times(V\times V)$ and hence the class $pr_3$ exists by Lemma 2 and the Axiom of Product by $V$. $\quad\square$

Lemma 8. For any functions $F,G$ the class $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}=dom[F\cap G]$ exists. $\quad\square$

Lemma 8. For any functions $F,G$ the class $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}$ exists.

Proof. Observe that $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}=dom[F\cap G]$ and apply the Axioms of Intersection and Domain. $\quad\square$

The idea is to prove that the function $f:((x,y),z))\mapsto ((x,z),y)$ exists (as a class) and then observe that for any class $X$, the class $\{((x,y),z):((x,z),y)\in X\}$ coincides with the image $f[X]$, which is equal to $dom((f\cap (X\times V))^{-1})$ so exists by application of Axioms of Product, Intersection, Inversion, and Domain. As was observed by Emil Jeřábek in his comment the Axiom of Intersection follows from the Axiom of Complement because $X\cap Y=X\setminus(X\setminus Y)$ for any classes $X,Y$.

Proof. By Lemma 1, the class $S=\{(x,y):x\subseteq y\}$ exists. Since $I=S\cap\pi_2[S]$ (by the Axiom of Extensionality), the class $I$ exists by the Axioms of Inversion and Intersection.

Proof. Observe that $p_1=\{(x,y):\exists a\exists b\;x=(a,b),\;y=a\}=dom[A]$ where $A=\{((x,y),(a,b)):x=(a,b),\;y=a\}$.

Write $A$ as $A=A_1\cap A_2$, where $A_1=\{((x,y),(a,b)):x=(a,b)\}$ and $A_2=\{((x,y),(a,b)):y=a\}$.

Observe that $\pi_3[A_1]=\{(((a,b),x),y):x=(a,b)\}=\{((a,b),x):x=(a,b)\}\times V=(V^2\cap I)\times V$, which implies that $A_1$ exists. Here $V^2=V\times V$.

Observe that $\pi^2_3[A_2]=\{((y,(a,b)),x):y=a\}=\{(y,(a,b)):y=a\}\times V=B\times V$, where $B=\{(y,(a,b)):y=a\}$. Next, $\pi_2[B]=\{((a,b),y):y=a\}$, $\pi_3[\pi_2[B]]=\{((y,a),b):y=a\}=I\times V$. Therefore, the classes $B$ and $A_2$ exist and the class $p_1$ exist, too.

Proof. Observe that $p_2=\{(x,y):\exists a\exists b\;(x=(a,b)\;\wedge\;y=b)\}=dom[A]$ where $A=\{((x,y),(a,b)):x=(a,b),\;y=b\}$.

Write $A$ as $A=A_1\cap A_2$, where $A_1=\{((x,y),(a,b)):x=(a,b)\}$ and $A_2=\{((x,y),(a,b)):y=b\}$.

Repeating the argument of the proof of Lemma 4, we can show that the class $A_1$ exists.

Observe that $\pi^2_3[A_2]=\{((y,(a,b)),x):y=b\}=\{(y,(a,b)):y=b\}\times V=B\times V$, where $B=\{(y,(a,b)):y=b\}$. Next, $\pi_2[B]=\{((a,b),y):y=b\}$, $\pi^2_3[\pi_2[B]]=\{((b,y),a):y=b\}=I\times V$. Therefore, the classes $B$ and $A_2$ exist and the class $p_2$ exist, too.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=a\}=\{(y,((a,b),c)):y=a\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=a\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=a\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=a\}=C\times V$ where $C=\{(y,(a,b)):y=a\}$. Observe that $\pi_2[C]=\{((a,b),y):y=a\}$ and $\pi_3[\pi_2[C]]=\{((y,a),b):y=a\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ exist and so does the class $pr_1=dom[A_1\cap A_2]$.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=b\}=\{(y,((a,b),c)):y=b\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=b\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=b\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=b\}=C\times V$ where $C=\{(y,(a,b)):y=b\}$. Observe that $\pi_2[C]=\{((a,b),y):y=b\}$ and $\pi_3^2[\pi_2[C]]=\{((b,y),a):b=y\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ and finally $pr_2$ exist.

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=c\}=\{(y,((a,b),c)):y=c\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=c\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=c\}$, $\pi^2_3[\pi_2[B]]=\{((c,y),(a,b)):c=y\}=I\times (V\times V)$. Then $A_2$ and exists and so does $pr_3$.

Lemma 8. For any functions $F,G$ the class $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}=dom[F\cap G]$ exists.

Then the classes $A_1$ and $A_2$ exist and so does the function $F\circ G$.

Proof. Observe that \begin{multline*} f=\{(a,b):a,b\in V^3,\;pr_1(a)=pr_1(b), \;pr_2(a)=pr_3(b),\;pr_3(a)=pr_2(b)\}=\\ \{x\in V^3{\times}V^3:pr_1{\circ}p_1(x)=pr_1{\circ}p_2(x),\; pr_2{\circ}p_1(x)=pr_3{\circ} p_2(x),\;pr_3{\circ} p_1(x)=pr_2{\circ} p_2(x)\}\end{multline*} and apply Lemmas 3--9.

The idea is to prove that the function $f:((x,y),z))\mapsto ((x,z),y)$ exists (as a class) and then observe that for any class $X$, the class $\{((x,y),z):((x,z),y)\in X\}$ coincides with the image $f[X]$, which is equal to $dom((f\cap (X\times V))^{-1})$ so exists by application of Axioms of Product, Intersection, Inversion, and Domain. As was observed by Emil Jeřábek in his comment, the Axiom of Intersection follows from the Axiom of Complement because $X\cap Y=X\setminus(X\setminus Y)$ for any classes $X,Y$.

Proof. By Lemma 1, the class $S=\{(x,y):x\subseteq y\}$ exists. Since $I=S\cap\pi_2[S]$ (by the Axiom of Extensionality), the class $I$ exists by the Axioms of Inversion and Intersection. $\quad\square$

The short proofs of the following two lemmas were suggested by Pace Nielsen in his comments below.

Proof. Observe that $\pi_3[p_1]=\{((a,a),b):a,b\in V\}=I\times V$, so the classes $\pi_3[p_1]$ and $p_1=\pi_3^2[\pi_3[p_1]]$ exist. $\quad\square$

Proof. Observe that $\pi^2_3[p_2]=\{((b,b),a):a,b\in V\}=I\times V$, so the class $p_2$ exists. $\quad\square$

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=a\}=\{(y,((a,b),c)):y=a\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=a\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=a\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=a\}=C\times V$ where $C=\{(y,(a,b)):y=a\}$. Observe that $\pi_2[C]=\{((a,b),y):y=a\}$ and $\pi_3[\pi_2[C]]=\{((y,a),b):y=a\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ exist and so does the class $pr_1=dom[A_1\cap A_2]$. $\quad\square$

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=b\}=\{(y,((a,b),c)):y=b\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=b\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=b\}$, $\pi_3[\pi_2[B]]=\{((y, (a,b)),c):y=b\}=C\times V$ where $C=\{(y,(a,b)):y=b\}$. Observe that $\pi_2[C]=\{((a,b),y):y=b\}$ and $\pi_3^2[\pi_2[C]]=\{((b,y),a):b=y\}=I\times V$. Therefore, the classes $C,B$ and $A_2$ and finally $pr_2$ exist. $\quad\square$

Observe that $\pi^2_3[A_2]=\{((y,((a,b),c)),x):y=c\}=\{(y,((a,b),c)):y=c\}\times V=B\times V$, where $B=\{(y,((a,b),c)):y=c\}$. Next, $\pi_2[B]=\{(((a,b),c),y):y=c\}$, $\pi^2_3[\pi_2[B]]=\{((c,y),(a,b)):c=y\}=I\times (V\times V)$. Then $A_2$ and exists and so does $pr_3$. $\quad\square$

Lemma 8. For any functions $F,G$ the class $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}=dom[F\cap G]$ exists. $\quad\square$

Then the classes $A_1$ and $A_2$ exist and so does the function $F\circ G$. $\quad\square$

Proof. Observe that \begin{multline*} f=\{(a,b):a,b\in V^3,\;pr_1(a)=pr_1(b), \;pr_2(a)=pr_3(b),\;pr_3(a)=pr_2(b)\}=\\ \{x\in V^3{\times}V^3:pr_1{\circ}p_1(x)=pr_1{\circ}p_2(x),\; pr_2{\circ}p_1(x)=pr_3{\circ} p_2(x),\;pr_3{\circ} p_1(x)=pr_2{\circ} p_2(x)\}\end{multline*} and apply Lemmas 3--9. $\quad\square$