\chapter{Further Primitives and Axioms}
\begin{axiom}\label{ax:ahchpgahpffgiheh} ${\unicdcdadad p q : {o} .  {{{{\mname{iff}}~{p}}~{q}}\unicdbdjdcd{{p}={q}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 00ac81fe17c156a4ac6f8a4b0f730686a7acf0e26a713a5d0e7f9aab342ef273 \\
Pure Prop Address: & TMT4ViLziW9cx8676T7siQNUsc4pLGajCAh \\
Theory Prop Id: & 1d1e565be0b2225dbdd84a1b9f843374545e89ad6f25ebf6856e801170f8d60b \\
Theory Prop Address: & TMK6YdqYUKB5vJfwfTMJNgJJGj1TmDiA7rj
\end{tabular}
\end{center}

\end{axiom}
{\bf{Primitive.}} The name $\mname{In}$ is a primitive term of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$. In particular it is ``Primitive 1'' in the Proofgold Egal theory.
\begin{definition}\label{def:dffhcgbh}

{\bf{Notation.}} We use $\in$ in infix notation for $\mname{In}$.

We define $\mname{Subq}$ to be ${\uniddcgcg A B .  {\unicdcdadad x \in {A} .  {{x} \in {B}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 81c0efe6636cef7bc8041820a3ebc8dc5fa3bc816854d8b7f507e30425fc1cef \\
Pure Object Address: & TMbQvibiSdPYTcyHirAiT7dojaZd9QVHnnx \\
Theory Object Id: & 317007aa687cfc3fa6d33a4d45b72e2b84878595f194108dee11852a04950639 \\
Theory Object Address: & TMJciJ4WVfdZbE7XT2SUcAkkoSYiF2gabRX
\end{tabular}
\end{center}

{\bf{Notation.}} We use $\subseteq$ in infix notation for $\mname{Subq}$.

\end{definition}
\begin{axiom}\label{ax:dhfgehpffgiheh} ${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{Y} \subseteq {X}}\unicdbdjdcd{{X}={Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b3b6981b6de9a71189167e6208f1fa2be38ade4bd2a77084c6878323e6d97ab9 \\
Pure Prop Address: & TMP6dV9kMfpLcfVgkH1rTbsurTnQKfFkFUf \\
Theory Prop Id: & 21238ac2a61503233d86f0ab5bbd1cfebd49fecaa7aa3a131715c5e08003430e \\
Theory Prop Address: & TMQ3CJdXpjT9Vyjdd8x58bzAfVa2uHKMmnZ
\end{tabular}
\end{center}

\end{axiom}
\begin{axiom}\label{ax:jeogpfjgogeg} ${\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad X : {\iota} .  {{({\unicdcdadad x \in {X} .  {{P}~{x}}})}\unicdbdjdcd{{P}~{X}}}})}\unicdbdjdcd{\unicdcdadad X : {\iota} .  {{P}~{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 04521121bc85ca3c89ee96767237629584fc96b34de1cf1a3f790ea4af4b0047 \\
Pure Prop Address: & TMZDd5XWnW8qoDTqVGuvgh8AQGEhcN5haVH \\
Theory Prop Id: & 20faa51007fd5aff9dc54e343b9c7b57fab2eb829c71a0daa2e90c858707d2b7 \\
Theory Prop Address: & TMMzAhfU4QKJhywTdGXVuR4P8u6KoKixxYw
\end{tabular}
\end{center}

\end{axiom}
{\bf{Notation.}} We use $\bindfgihjgdhehdh x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{ex}}$ and handling $\in$ or $\subseteq$ ascriptions using $
{\mname{and}}$.
{\bf{Primitive.}} The name $\mname{Empty}$ is a primitive term of type ${\iota}$.
In particular it is ``Primitive 2'' in the Proofgold Egal theory.
\begin{axiom}\label{ax:fengahehjhbeih} ${\preoh{{\unicdcdaddd x : {\iota} .  {{x} \in {\mname{Empty}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4da93150e41630a98ea3fc30e9bc894dee0da4364b020ac8ee0a79d04508434f \\
Pure Prop Address: & TMQMLLe8Cz5vwfXB4uUFfsKFVfvwBMf4VPJ \\
Theory Prop Id: & c7b0d7f466fd9528f6264e7a3a9eaeff8c18159e8679b3d6b840d2689bda8486 \\
Theory Prop Address: & TMaPKWsC7HDHhrC2zYBmYcX19RqLy2VefbW
\end{tabular}
\end{center}

\end{axiom}
{\bf{Primitive.}} The name $\mname{Union}$ is a primitive term of type ${{\iota}\unicdbdjdcd{\iota}}$.
In particular it is ``Primitive 3'' in the Proofgold Egal theory.
\begin{axiom}\label{ax:ffogjgpgogfebh} ${\unicdcdadad X x .  {{{x} \in {{\mname{Union}}~{X}}}\unicdbdjded{\unicdcdaddd Y .  {{{x} \in {Y}}\unicdcdcdhd{{Y} \in {X}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bf4c263ac4776c12ed6de40b226c687445f1e634eddf121ad52b2d095224ec74 \\
Pure Prop Address: & TMHRWvQi72bggXNdrukFL23tqhkHk6iri2y \\
Theory Prop Id: & 40660fae1988a12c0dd433fed65b5971371ce274cfa7acb0152f6c8b11856323 \\
Theory Prop Address: & TMdiuFh9LBKb2nXjbQi7GzQCn57wX2izbEV
\end{tabular}
\end{center}

\end{axiom}
{\bf{Primitive.}} The name $\mname{Power}$ is a primitive term of type ${{\iota}\unicdbdjdcd{\iota}}$.
Specifically it is ``Primitive 4'' in the Proofgold Egal theory.
\begin{axiom}\label{ax:afpghhfgchfebh} ${\unicdcdadad X Y : {\iota} .  {{{Y} \in {{\mname{Power}}~{X}}}\unicdbdjded{{Y} \subseteq {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 746e5a9564518580f673371a7891c1db2e38c91762155f302694c6b4cbf7c649 \\
Pure Prop Address: & TMTzabXXxRmuTxrdG42VtpMDWCUmgK2UMgY \\
Theory Prop Id: & d67d718c245e91b738c984751e77f84e6db2b59131a6dd3dbf033e5c5b151dc0 \\
Theory Prop Address: & TMbRJTDNmcR6KZC6t4TGXakKw4XSAYS3VN8
\end{tabular}
\end{center}

\end{axiom}
{\bf{Primitive.}} The name $\mname{Repl}$ is a primitive term of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$.
Specifically it is ``Primitive 5'' in the Proofgold Egal theory.

{\bf{Notation.}} We write $\mname{Repl}~A~(\lambda x.s)$ as $\{s|x\in A\}$.

\begin{axiom}\label{ax:cffgahmgfebh} ${\unicdcdadad A : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y : {\iota} .  {{{y} \in {\{{{F}~{x}}|x \in {A}\}}}\unicdbdjded{\unicdcdaddd x \in {A} .  {{y}={{F}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4f2357276dc7f58ae12c278fb7f133f1de0a4e899d0a1b4df22db544ef8fbfea \\
Pure Prop Address: & TMHvGDzbjKwgKUfmhz4YstLTy6FK6VEf8VX \\
Theory Prop Id: & 471122ee9aecdb9185d0ed855c4fd074596525d6ade7150ea945d05f732c1d91 \\
Theory Prop Address: & TMQwYTqizk3ouisSfLQUbv5JP258W4VhxxV
\end{tabular}
\end{center}

\end{axiom}
\begin{definition}\label{def:efchbgogdhdffgeh}
We define $\mname{TransSet}$ to be ${\uniddcgcg U : {\iota} .  {\unicdcdadad x \in {U} .  {{x} \subseteq {U}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 538bb76a522dc0736106c2b620bfc2d628d5ec8a27fe62fc505e3a0cdb60a5a2 \\
Pure Object Address: & TMFFkFhggUWb8iaKbBVFF2NXQtBDp9ocvey \\
Theory Object Id: & e69f92130adf04e6fb850fe93c130a82c6a84226e2914139b5b46a4c8b46dd59 \\
Theory Object Address: & TMaE1Wfu3Ekit1RP2q2rs1eExhVT4eYQUWZ
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ffogjgpgogpfdgmgpgdhfgeg}
We define $\mname{Union\_closed}$ to be ${\uniddcgcg U : {\iota} .  {\unicdcdadad X : {\iota} .  {{{X} \in {U}}\unicdbdjdcd{{{\mname{Union}}~{X}} \in {U}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 57561da78767379e0c78b7935a6858f63c7c4be20fe81fe487471b6f2b30c085 \\
Pure Object Address: & TMGQhGvaoAR8Ac54JYsvH3PiWjPoz8NS8J6 \\
Theory Object Id: & e45ed946b4201c2ac3bce08c594bcc5b37e16935b9de8d06f9515256bfcb6c5d \\
Theory Object Address: & TML288688fkgDpJdibigbTFnrScrqv2iKt8
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:afpghhfgchpfdgmgpgdhfgeg}
We define $\mname{Power\_closed}$ to be ${\uniddcgcg U : {\iota} .  {\unicdcdadad X : {\iota} .  {{{X} \in {U}}\unicdbdjdcd{{{\mname{Power}}~{X}} \in {U}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8b9cc0777a4e6a47a5191b7e6b041943fe822daffc2eb14f3a7baec83fa16020 \\
Pure Object Address: & TMGEQQpyASUMyKRHqWbnFXopjtYsATE5AVk \\
Theory Object Id: & d2954ea0f8a59a40ddc3fc5be9d473a03e8b92e4a279ea7e2bf10debed186ffd \\
Theory Object Address: & TMNbYYR8P3gh4AeJAfTdNEMMkiD5HvA97jx
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:cffgahmgpfdgmgpgdhfgeg}
We define $\mname{Repl\_closed}$ to be
$${\uniddcgcg U : {\iota} .  {\unicdcdadad X : {\iota} .  {{{X} \in {U}}\unicdbdjdcd{\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{F}~{x}} \in {U}}}})}\unicdbdjdcd{{\{{{F}~{x}}|x \in {X}\}} \in {U}}}}}}}$$
of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 5574bbcac2e27d8e3345e1dc66374aa209740ff86c1db14104bc6c6129aee558 \\
Pure Object Address: & TMHsmhDUjBaGfXeB9XmeViaPhpFM3GPGFEK \\
Theory Object Id: & 5135346e3c2b9f78fd2ca0f8dc77f2075a100d43dfdecf64bc2792a54493f446 \\
Theory Object Address: & TMFer2uiF5iECeDKX8Yjf4jvbfj2RQYen9J
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:kfgepfdgmgpgdhfgeg}
We define $\mname{ZF\_closed}$ to be ${\uniddcgcg U : {\iota} .  {{{{\mname{Union\_closed}}~{U}}\unicdcdcdhd{{\mname{Power\_closed}}~{U}}}\unicdcdcdhd{{\mname{Repl\_closed}}~{U}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1bd4aa0ec0b5e627dce9a8a1ddae929e58109ccbb6f4bb3d08614abf740280c0 \\
Pure Object Address: & TMK8id4rjoGzRQvGv2RVDkaCpE2gvidq2jS \\
Theory Object Id: & e1eccf55c627a83d82a0c5fbb2d8effe908afbba6259c3a3a9f7af4839904407 \\
Theory Object Address: & TMKM8HgiAgaT2ShpWewk4PuTK8LpKuESdvs
\end{tabular}
\end{center}

\end{definition}
{\bf{Primitive.}} The name $\mname{UnivOf}$ is a primitive term of type ${{\iota}\unicdbdjdcd{\iota}}$.
In particular it is ``Primitive 6'' in the Proofgold Egal theory.
\begin{axiom}\label{ax:ffogjgghpeggpfjeog} ${\unicdcdadad N : {\iota} .  {{N} \in {{\mname{UnivOf}}~{N}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & efcc1652fa565b11ad9b7e6b61992946e170a56766124011245e25a95ef533d8 \\
Pure Prop Address: & TMWDMXfHXNT3hXXgPN8FdFXa6TtH5VEC8L2 \\
Theory Prop Id: & e805d44e6e3b129108fe3a5d7b86456ab1ded7fbabdb1e013db339c19e74fc3c \\
Theory Prop Address: & TMXQAwXZaXUD3yTSAm1fLH7g2HqyDMYutzR
\end{tabular}
\end{center}

\end{axiom}
\begin{axiom}\label{ax:ffogjgghpeggpfefchbgogdhdffgeh} ${\unicdcdadad N : {\iota} .  {{\mname{TransSet}}~{({{\mname{UnivOf}}~{N}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 05357566d69c1e942fba918ba630fe1befcd3b76747edaa23bf9e22c07e0bf80 \\
Pure Prop Address: & TMPFnHy6wH7xHdqPH1LVnFGKXNXBVDCGhcc \\
Theory Prop Id: & cf4f5cdd03fb3fcd9b880d27f1bb10dfa697dda82fb891d4f01e8901f99e0ddd \\
Theory Prop Address: & TMQDPgN5NEyK5uGnLoLPsCtuYVhgM8BFwd8
\end{tabular}
\end{center}

\end{axiom}
\begin{axiom}\label{ax:ffogjgghpeggpfkfgepfdgmgpgdhfgeg} ${\unicdcdadad N : {\iota} .  {{\mname{ZF\_closed}}~{({{\mname{UnivOf}}~{N}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 770e356024df94789dc767ad29154fb817b6339b6526f6b4826cc678ae6937ab \\
Pure Prop Address: & TMUaRKj3xqMnJ3tpKZ46beaVE82Vps7qYVG \\
Theory Prop Id: & 0e736334ea6ea7d6454eede353e88ba0fa7a5e4c3a17f6c90921a2414dab6d08 \\
Theory Prop Address: & TMK8JSDxgUygbLA49dTtQCjnRY2ijj3pG6u
\end{tabular}
\end{center}

\end{axiom}
\begin{axiom}\label{ax:ffogjgghpeggpfnejgog} ${\unicdcdadad N U : {\iota} .  {{{N} \in {U}}\unicdbdjdcd{{{\mname{TransSet}}~{U}}\unicdbdjdcd{{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{{{\mname{UnivOf}}~{N}} \subseteq {U}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 042dda2b34a2ebfa193a104324faf5219666788a71551ab9dd079136a7c6281d \\
Pure Prop Address: & TMSbghKuyRptdLDe7mXjA1e8YRJUc3PRgkx \\
Theory Prop Id: & 1f793348811ae94e9d72c764a3e780c39a9a2f45f55507133ecc732e15133ce6 \\
Theory Prop Address: & TMGeTmqMVx11mKzRV46CRSj6xUcaf13udQk
\end{tabular}
\end{center}

\end{axiom}
