User:RJGray/Math

Ordinals

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(X)\;\And \;u\in X\implies Seg_{E}(X,u)=u.\\&{\textbf {Proof.}}\;\;Pred_{E}(u)=u{\text{ by definition of }}E.\;\;u\subseteq X{\text{ since }}Trans(X).\\&\therefore Seg_{E}(X,u)=X\cap Pred_{E}(u)=X\cap u=u.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(Y)\;\And \;X\subset Y\;\And \;Trans(X)\implies X\in Y.\\&{\textbf {Proof.}}\;\;{\text{Let }}u=least(Y\setminus X).\\&x\in u\implies x\in X:\;\;{\text{Since }}u=least(Y\setminus X),\,x\in X.\\&x\in X\implies x\in u:\;\;{\text{Let }}x\in X.\;\;{\text{ If }}x=u,{\text{ then }}x\notin X.\;\;{\text{ Contradiction.}}\\&\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad \!{\text{If }}u\in x,{\text{ then }}Trans(X)\implies u\in X.\;\;{\text{ Contradiction.}}\;\;\therefore x\in u.\\&{\text{By extensionality, }}X=u.\;\;\therefore X\in Y.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(X)\;\And \;Ord(Y)\implies {\text{Only one of the following holds: }}X\in Y,\,X=Y,\,Y\in X.\\&{\textbf {Proof.}}\;\;Trans(X)\;\And \;Trans(Y)\implies Trans(X\cap Y).\\&{\text{Assume }}X\nsubseteq Y\;\And \;Y\nsubseteq X.\;\;{\text{ Then }}X\cap Y\neq X\;\And \;X\cap Y\neq Y.\;{\text{ Hence, }}X\cap Y\subset X\;\And \;X\cap Y\subset Y.\\&{\text{By the previous theorem, }}Ord(X)\;\And \;Trans(X\cap Y)\;\And \;X\cap Y\subset X\implies X\cap Y\in X.\\&{\text{Similarly, }}X\cap Y\in Y.{\text{ Thus, }}X\cap Y\in X\cap Y,{\text{ which contradicts regularity}}.\\&\therefore X\subseteq Y\lor Y\subseteq X,{\text{ which implies }}X\subset Y\lor X=Y\lor Y\subset X.\\&{\text{There are 3 ways for 2 of these 3 to be true: }}(X\subset Y\;\And \;X=Y)\lor (X=Y\;\And \;Y\subset X)\lor (X\subset Y\;\And \;Y\subset X).\\&{\text{Each of these implies }}X\subset X,{\text{ which is a contradiction. Therefore, only one of the three holds.}}\\&{\text{By the previous theorem, this implies that only one of the following holds: }}X\in Y,\,X=Y,\,Y\in X.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;E\,Connex\,On.\\&{\textbf {Proof.}}\;\;{\text{Implied by the previous theorem.}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(A)\;\And \;X\in A\implies Ord(X).\\&{\textbf {Proof.}}\;\;Ord(A)\implies X\subseteq A.\quad \therefore E\,Well\,A\implies E\,Well\,X.\\&{\text{Let }}Z\in Y\in X\in A.\quad Trans(A)\implies Z,Y,X\in A.\\&E\,Well\,A\;\And \;Z\in Y\in X\implies Z\in X.\quad \therefore Trans(X).\\&\therefore E\,Well\,X\;\And \;Trans(X)\implies Ord(X).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(A)\implies A\subseteq On.\\&{\textbf {Proof.}}\;\;{\text{Let }}X\in A.\;{\text{ Since }}Ord(A),{\text{ the previous theorem implies }}Ord(X).\\&{\text{Since }}X{\text{ is a set, }}X\in On.\quad \therefore A\subseteq On.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Trans(On).\\&{\textbf {Proof.}}\;\;{\text{Since }}A\in On{\text{ implies }}Ord(A),{\text{ the previous theorem implies }}A\subseteq On.\quad \therefore Trans(On).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(On).\\&{\textbf {Proof.}}\;\;{\text{Follows from earlier theorems that imply }}E\,Connex\,On\;\And \;Trans(On).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;\forall X(X\subseteq On\implies E\,Well\,X).\\&{\textbf {Proof.}}\;\;Ord(On)\implies E\,Well\,On\implies E\,Well\,X{\text{ for all }}X\subseteq On.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;\forall x(x\in A\implies Trans(x))\implies Trans(\cup A).\\&{\textbf {Proof.}}\;\;{\text{Let }}u\in v\in \cup A.\;{\text{ There exists a }}w{\text{ such that }}v\in w\in A.\\&Trans(w)\;\And \;u\in v\in w\implies u\in w.\\&{\text{Since }}u\in w\in A\implies u\in \cup A,{\text{ we have }}Trans(\cup A).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;A\subseteq T\;\And \;Trans(T)\implies \cup A\subseteq T.\\&{\textbf {Proof.}}\;\;{\text{Let }}u\in \cup A.\;{\text{ Then there exists a }}v{\text{ such that }}u\in v\in A.\\&A\subseteq T\implies u\in v\in T.\;\;Trans(T)\implies u\in T.\quad \therefore \cup A\subseteq T.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;A\subseteq On\implies Ord(\cup A).\\&{\textbf {Proof.}}\;\;{\text{Use last two theorems. First implies}}\;Trans(\cup A){\text{ since }}\forall x[x\in A\subseteq On\implies Trans(x)].\\&{\text{Second implies}}\;E\,Well\cup \!A{\text{ since }}A\subseteq On\;\And \;Trans(On)\implies \cup A\subseteq On.\\&\therefore Ord(\cup A).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;\alpha +1=\alpha \cup \{\alpha \}{\text{ is the ordinal that follows }}\alpha .\\&{\textbf {Proof.}}\;\;Trans(\alpha +1):\beta \in \alpha \cup \{\alpha \}\implies \beta \in \alpha \lor \beta =\alpha .\\&\quad {\text{Now }}\beta \in \alpha \implies \beta \subseteq \alpha {\text{ and }}\beta =\alpha \implies \beta \subseteq \{\alpha \}.\quad \therefore \beta \subseteq \alpha \cup \{\alpha \}.\\&E\,Well\,\alpha +1{\text{ since we have just added one set to the end of the well-ordered set }}\alpha .\quad \therefore Ord(\alpha +1).\\&{\text{Next we prove: }}\alpha <\beta \implies \alpha +1\leq \beta .\\&\alpha \in \beta \implies \alpha \subseteq \beta .\;{\text{ Also, }}\alpha \in \beta \implies \{\alpha \}\subseteq \beta \quad \therefore \alpha \cup \{\alpha \}\subseteq \beta .\\&{\text{This implies }}\alpha \cup \{\alpha \}\in \beta \lor \alpha \cup \{\alpha \}=\beta .\quad \therefore \alpha \cup \{\alpha \}\leq \beta .\\&{\text{Gödel proves }}\beta \in \alpha +1\implies \beta \leq \alpha :\beta \in \alpha \cup \{\alpha \}\implies \beta \in \alpha \lor \beta =\alpha \implies \beta \leq \alpha .\\\\\end{alignedat}}$

Functions on Ordinals

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;{\text{If }}\beta >\alpha \implies F(\beta )>F(\alpha ),{\text{ then }}\forall \alpha (F(\alpha )\geq \alpha ).\\&{\textbf {Proof.}}\;\;{\text{By contradiction. Assume }}\exists \alpha (F(\alpha )<\alpha )\;{\text{ and let }}\alpha =least\,\{\alpha :F(\alpha )<\alpha \}.\;{\text{ Then }}F(\alpha )=\beta <\alpha .\\&{\text{However, }}F(\beta )\geq \beta \;\And \;F(\alpha )>F(\beta )\implies F(\alpha )>\beta .\;{\text{ Contradiction.}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(X)\;\And \;Ord(Y)\;\And \;F\,Isom_{E,E}(X,Y)\implies X=Y\;\And \;F=I\upharpoonright X.\\&{\textbf {Proof.}}\;\;{\text{Let }}\alpha =least\,\{\alpha \in X:F(\alpha )\neq \alpha \}\;{\text{ and let }}F(\alpha )=\beta .\\&\beta <\alpha :{\text{Then }}F(\alpha )=\beta =F(\beta ),\;{\text{ contradicting }}F{\text{ being one-to-one}}.\\&\beta >\alpha :{\text{ If }}\gamma <\alpha ,{\text{ then }}F(\gamma )=\gamma <\alpha .\;{\text{ If }}\gamma \geq \alpha ,{\text{ then }}F(\gamma )\geq F(\alpha )=\beta >\alpha ,{\text{ contradicting }}F{\text{ being onto.}}\\&{\text{Thus, }}\forall \alpha \in X(F(\alpha )=\alpha ).\;{\text{ Since }}F{\text{ is an isomorphism, }}Y=Rng(F)=X\;\And \;F=I\upharpoonright X.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;\forall G\,\exists !F\,[F\,Fn\,On\;\And \;\forall \alpha (F(\alpha )=G(F\upharpoonright \alpha )].\\&{\textbf {Proof.}}\;\;{\text{Strategy: Define class }}K{\text{ consisting of all functions }}f{\text{ that approximate }}F{\text{ on }}\beta .\\&{\text{Let: }}f\in K\iff \exists \beta [f\,Fn\,\beta \;\And \;\forall \alpha (\alpha \in \beta \implies f(\alpha )=G(f\upharpoonright \alpha ))]\\&f_{1}\,Fn\,\beta _{1}\in K\;\And \;f_{2}\,Fn\,\beta _{2}\in K\;\And \;\beta _{1}<\beta _{2}\implies f_{1}\subseteq f_{2}:\\&\quad {\text{Assume conclusion is false. Let }}\alpha =least\{\gamma :f_{1}(\gamma )\neq f_{2}(\gamma )\}.\\&\quad {\text{However, }}f_{1}(\alpha )=G(f_{1}\upharpoonright \alpha ))=G(f_{2}\upharpoonright \alpha ))=f_{2}(\alpha ),{\text{contradicting our assumption.}}\\&\quad \therefore f_{1}\subseteq f_{2}.\\&\forall \alpha (\exists !f(f\in K\;\And \;f\,Fn\,\alpha \;\And \;\forall \beta <\alpha (F(\beta )=G(F\upharpoonright \beta )]):\\&\quad {\text{Assume false and let }}\alpha {\text{ be least such that it is false. However, since }}\alpha {\text{ is least, we can define}}\\&\quad {\text{a function }}f{\text{ by: }}h=\cup \{g\in K:\beta <\alpha \land g\,Fn\,\beta \};\;f=h\cup \{\langle \alpha ,G(h\upharpoonright \alpha )\rangle \},\\&\quad {\text{contradicting our assumption.}}\\&{\text{Let }}F=\cup K.\;\;F\,Fn\,On\;\And \;\forall \alpha (F(\alpha )=G(F\upharpoonright \alpha )):\\&\quad {\text{The first statement proved above implies that }}F{\text{ is a function satisfying the recursive definition.}}\\&\quad {\text{The second statement implies that }}Dom(F)=On.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Pr(A)\;\And \;W\,Well\,A\;\And \;{\text{All proper initial segments of }}A{\text{ are sets}}\implies Isom_{E,W}(On,A).\\&{\textbf {Proof.}}\;\;{\text{Define: }}F(\alpha )=least(A\setminus F\upharpoonright \alpha ).\\&{\text{If }}\forall \beta (\beta <\alpha \implies Seg_{W}(A,F(\beta ))=F\upharpoonright \beta {\text{ is a proper initial segment of }}A),\\&{\text{then }}Seg_{W}(A,F(\alpha ))=F\upharpoonright \alpha {\text{ is a proper initial segment of }}A.\\&\quad {\text{Proof by transfinite induction:}}\\&\quad \alpha =0:Seg_{W}(A,F(0))=\emptyset =F\upharpoonright \emptyset ,{\text{ which is a proper initial segment.}}\\&\quad \alpha =\beta +1:Seg_{W}(A,F(\alpha ))=Seg_{W}(A,F(\beta ))\cup \{F(\beta )\}=F\upharpoonright \beta \cup \{F(\beta )\}=F\upharpoonright \alpha ,\\&\quad {\text{which is a proper initial segment since }}F(\beta ){\text{ is ordinal following ordinals in }}Seg_{W}(A,F(\beta )).\\&\quad \alpha =Lim\{\beta :\beta <\alpha \}:Seg_{W}(A,F(\alpha ))=\cup \{Seg_{W}(A,F(\beta )):\beta <\alpha \}=\cup \{F\upharpoonright \beta :\beta <\alpha \}=F\upharpoonright \alpha ,\\&\quad {\text{which is a proper initial segment since }}F(\alpha ){\text{ is ordinal following ordinals in }}\cup \{Seg_{W}(A,F(\beta )):\beta <\alpha \}.\\&F{\text{ preserves ordering : }}\,\beta <\alpha \implies F(\beta )\,W\,F(\alpha ):F(\beta )\in F\upharpoonright \alpha =Seg_{W}(A,F(\alpha ))\implies F(\beta )\,W\,F(\alpha ).\\&Dom(F)=On:{\text{ Let }}\alpha \in On.\;{\text{ By replacement }}F\upharpoonright \alpha {\text{ is a set. Since }}A{\text{ is a proper class, }}A\setminus F\upharpoonright \alpha \\&\quad {\text{is a proper class, so it is non-empty. Thus, }}\;F(\alpha )=least(A\setminus F\upharpoonright \alpha ){\text{ is defined.}}\quad \therefore Dom(F)=Ord.\\&Rng(F)=A:{\text{ Assume }}Rng(F)\subset A.\;\;{\text{ Let }}y=least\{x\in A:x\notin Rng(F)\}{\text{ and let }}X=\{x:xWy\}.\\&\quad {\text{Since }}X{\text{ is a proper initial segment, it is a set.}}\\&\quad F{\text{ is a bijection from }}On{\text{ to }}X,{\text{ so }}F^{-1}{\text{ is a bijection from }}X{\text{ to }}Ord.\\&\quad {\text{By replacement, }}F^{-1}[X]=On{\text{ is a set, contradicting }}On{\text{ being a proper class.}}\\&\quad \therefore Rng(F)=A.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;{\text{If }}a{\text{ is a set and }}W\,Well\,a,{\text{ then }}\exists \alpha (\alpha \in On\land Isom_{E,W}(\alpha ,a)).\\&{\textbf {Proof.}}\;\;{\text{Define: }}f(\beta )=least(a\setminus f\upharpoonright \beta ).\\&{\text{Same proof of properties as in last theorem with the difference that the construction terminates at }}\alpha .\\&{\text{Assume it does not terminate at any ordinal number }}\alpha .\;{\text{Then }}f{\text{ is a bijection from }}On{\text{ to a subset of }}a.\\&{\text{So }}f^{-1}{\text{ is a bijection from a subset of }}a{\text{ to }}On.\\&{\text{By replacement, }}f^{-1}[a]=On{\text{ is a set, contradicting }}On{\text{ being a proper class.}}\\&\therefore \exists \alpha (\alpha \in On\land Isom_{E,W}(\alpha ,a)).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;(\alpha ,\beta )\;Le\;(\gamma ,\delta )\iff \beta <\delta \lor (\beta =\delta \land \alpha <\gamma ).\\&{\textbf {Definition.}}\;\;(\alpha ,\beta )\;R\;(\gamma ,\delta )\iff Max(\alpha ,\beta )<Max(\gamma ,\delta )\lor (Max(\alpha ,\beta )=Max(\gamma ,\delta )\land (\alpha ,\beta )\;Le\;(\gamma ,\delta ))\\&{\textbf {Theorem.}}\;\;R{\text{ well-orders }}On^{2}.\\&{\textbf {Proof.}}\;\;R\;Connex\;On^{2}:{\text{ Follows from }}Max(\alpha ,\beta )<Max(\gamma ,\delta ),Max(\alpha ,\beta )=Max(\gamma ,\delta ),\\&\quad {\text{ or }}Max(\alpha ,\beta )>Max(\gamma ,\delta );{\text{ and similar inequalities holding between }}\beta {\text{ and }}\delta ,{\text{ and }}\alpha {\text{ and }}\gamma .\\&R\;Well\;On^{2}:{\text{ Let }}U\subseteq On^{2}.\\&\quad {\text{Let }}min_{1}=least\,\{Max(\alpha ,\beta ):(\alpha ,\beta )\in U\}{\text{ and let }}U_{1}=\{(\alpha ,\beta )\in U:Max(\alpha ,\beta )=min_{1}\}.\\&\quad {\text{Then }}\;\forall (\alpha ,\beta )\in U_{1}(Max(\alpha ,\beta )=min_{1}){\text{ and }}\forall (\alpha ,\beta )\in U\setminus U_{1}[Max(\alpha ,\beta )>min_{1}).\\&\quad {\text{Let }}min_{2}=least\,\{\beta :(\alpha ,\beta )\in U_{1}\}{\text{ and let }}U_{2}=\{(\alpha ,\beta )\in U_{1}:\beta =min_{2}\}.\\&\quad {\text{Then }}\;\forall (\alpha ,\beta )\in U_{2}(\beta =min_{2}){\text{ and }}\forall (\alpha ,\beta )\in U_{1}\setminus U_{2}(\beta >min_{2}).\\&\quad {\text{Let }}min_{3}=least\,\{\alpha :(\alpha ,\beta )\in U_{2}\}{\text{ and let }}U_{3}=\{(\alpha ,\beta )\in U_{2}:\alpha =min_{3}\}.\\&\quad {\text{Then }}\;\forall (\alpha ,\beta )\in U_{3}(\alpha =min_{3}){\text{ and }}\forall (\alpha ,\beta )\in U_{2}\setminus U_{3}(\alpha >min_{3}).\\&\quad {\text{Now }}min=(min_{3},min_{2}){\text{ is the only member of }}U_{3}.\\&\quad {\text{Since }}min\in U_{3}\subseteq U_{2}\subseteq U_{1}\subseteq U,{\text{ the above properties imply }}min<(\alpha ,\beta ){\text{ for all }}(\alpha ,\beta )\in U\setminus U3.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Pr(On^{2})\;\And \;{\text{ All proper initial segments of }}(On^{2},R){\text{ are sets. Therefore, }}Isom_{E,R}(On,On^{2}).\\&{\textbf {Proof.}}\;\;Pr(On)\implies Pr(On^{2}).\\&{\text{Let }}S=Seg_{R}(On^{2},(\alpha ,\beta )){\text{ be a proper initial segment and let }}\delta =Max(\alpha ,\beta ).\\&S\subseteq Seg_{R}(On^{2},(\delta ,\delta )+1)\subseteq (\delta +1)\times (\delta +1),{\text{ which is a set.}}\quad \therefore S{\text{ is a set.}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;{\text{If }}\,F\,Isom_{E,<}(On,On^{2}){\text{ as defined above and }}P=F^{-1},{\text{ then }}P((\alpha ,\beta ))\geq max(\alpha ,\beta ).\\&{\textbf {Proof.}}\;\;{\text{This follows from: }}\;F(max(\alpha ,\beta ))\leq (max(\alpha ,\beta ),0)\leq (\alpha ,\beta )\\&\qquad \;{\text{since applying }}P{\text{ gives: }}\;max(\alpha ,\beta )\leq P((max(\alpha ,\beta ),0))\leq P((\alpha ,\beta )).\\&{\text{All we need to prove is: }}F(\alpha )\leq (\alpha ,0).\\&\quad \alpha =\beta +1:F(\beta +1)=F(\beta )+1\leq (\alpha ,0)+1\leq (\alpha +1,0).\\&\quad \alpha =Lim\{\beta :\beta <\alpha \}:\\&\quad \quad {\text{Lemma: }}{\text{ If }}F{\text{ is an isomorphism and }}a=Lim\{b:b<a\},{\text{ then }}F(a)=Lim\{F(b):b<a\}.\\&\quad \quad {\text{Proof: }}{\text{ If }}F{\text{ is an isomorphism and }}a=Lim\{b:b<a\},{\text{ then }}a{\text{ can be defined as }}\\&\quad \quad \quad a\neq least(A)\land \neg \exists b(a=b+1)\land a=least(A\setminus \{b:b<a\}).{\text{ Since }}F{\text{ is an isomorphism,}}\\&\quad \quad \quad F(a)\neq least(F(A))\land \neg \exists F(b)(F(a)=F(b)+1)\land F(a)=least(F(A)\setminus \{F(b):F(b)<F(a)\}).\\&\quad \quad \quad \therefore F(a)=Lim\{F(b):F(b)<F(a)\}=Lim\{F(b):b<a\}.\\&\quad \quad \therefore F(\alpha )=Lim\{F(\beta ):\beta <\alpha \}\leq Lim\{(\beta ,0):\beta <\alpha \}=(\alpha ,0).{\text{The last equality holds since }}\\&\quad \quad \quad Lim\{(\beta ,0):\beta <\alpha \}=least(On^{2}\setminus \cup \{seg_{R}(On^{2},(\beta ,0)):(\beta ,0)\,R\,(\alpha ,0)\})=(\alpha ,0).\\&{\text{Gödel's proof is much shorter: }}P((\alpha ,\beta ))\geq P((max(\alpha ,\beta ),0)).\;\;{\text{Let }}\gamma =max(\alpha ,\beta ).\\&\quad {\text{Because }}P((\gamma ,0)){\text{ is strictly increasing, }}P((\gamma ,0))\geq \gamma .\\&\quad \therefore P((\alpha ,\beta ))\geq P((max(\alpha ,\beta ),0))\geq max(\alpha ,\beta ).\\\\\end{alignedat}}$

Construction of L

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&(i,\alpha ,\beta )\;S\;(j,\gamma ,\delta )\iff (\alpha ,\beta )\;R\;(\gamma ,\delta )\lor ((\alpha ,\beta )=(\gamma ,\delta )\land i<j.\\\\&{\textbf {Theorem.}}&&Pr(8\times On^{2})\;\And \;{\text{ All proper initial segments of }}(8\times On^{2},S){\text{ are sets. Therefore, }}Isom_{E,S}(On,8\times On^{2}).\\&{\textbf {Proof.}}&&Pr(On)\implies Pr(8\times On^{2}).\\&&&{\text{Let }}A=Seg_{S}(8\times On^{2},(i,\alpha ,\beta )){\text{ be a proper initial segment and let }}\delta =Max(\alpha ,\beta ).\\&&&A\subseteq Seg_{S}(8\times On^{2},(8,\delta ,\delta )+1)\subseteq 8\times (\delta +1)\times (\delta +1),{\text{ which is a set.}}\quad \therefore A{\text{ is a set.}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&J\,Fn\,(8\times On^{2})\land Rng(J)=On\land i,j<8\implies [(i,\alpha ,\beta )\;S\;(j,\gamma ,\delta )\implies J((i,\alpha ,\beta ))<J((j,\gamma ,\delta ))].\\&{\textbf {Definition.}}&&{\text{For }}0\leq i\leq 7:\,J_{i}((\alpha ,\beta ))=J((i,\alpha ,\beta )).\\\\&{\textbf {Theorem.}}&&{\text{The }}Rng(J_{i}){\text{ are mutually exclusive and their union is }}On.\\&{\textbf {Proof.}}&&{\text{The ranges are mutually exclusive because }}J{\text{ is one-to-one.}}\\&&&{\text{The union of the ranges is }}On{\text{ because }}J{\text{ is onto }}On.\\\\\end{alignedat}}$

${\text{For any }}\gamma ,{\text{ there is a unique }}(i,\alpha ,\beta ){\text{ such that }}\gamma =J(i,\alpha ,\beta ).$
$\therefore {\text{ There are functions }}K_{1}{\text{ and }}K_{2}{\text{ on }}On{\text{ such that }}K_{1}(J_{i}(\alpha ,\beta ))=\alpha \;\And \;K_{2}(J_{i}(\alpha ,\beta ))=\beta .$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&(\alpha ,\gamma )\in K_{1}\iff \exists i<8\,\exists \beta \,(\gamma =J((i,\alpha ,\beta )))\land K_{1}\subseteq On^{2}.\\&{\textbf {Definition.}}&&(\beta ,\gamma )\in K_{2}\iff \exists i<8\,\exists \alpha \,(\gamma =J((i,\alpha ,\beta )))\land K_{2}\subseteq On^{2}.\\\\&{\textbf {Theorem.}}&&J_{i}((\alpha ,\beta ))\geq max(\alpha ,\beta ),\quad J_{i}((\alpha ,\beta ))>max(\alpha ,\beta ){\text{ for }}i>0,\\&&&K_{1}(\alpha )\leq \alpha ,\qquad \qquad \qquad \,K_{1}(\alpha )<\alpha {\text{ for }}\alpha \notin Rng(J_{0}),\\&&&K_{2}(\alpha )\leq \alpha ,\qquad \qquad \qquad \,K_{2}(\alpha )<\alpha {\text{ for }}\alpha \notin Rng(J_{0}).\\&{\textbf {Proof.}}&&J((i,\alpha ,\beta ))\geq J((i,(max(\alpha ,\beta ),0)).\\&&&{\text{Because }}J((i,(max(\alpha ,\beta ),0)){\text{ is strictly increasing, }}J((i,\gamma ,0))\geq \gamma .\\&&&\therefore {\text{For }}i>0:J((i,\alpha ,\beta ))>J((0,\alpha ,\beta ))\geq J((0,(max(\alpha ,\beta ),0))\geq max(\alpha ,\beta ).\\&&&{\text{Since for }}i>0:\;J((i,\alpha ,\beta ))>J((0,\alpha ,\beta ))\geq \alpha .\\&&&{\text{We have }}i>0:\;K_{1}(J((i,\alpha ,\beta )))>K_{1}(J((0,\alpha ,\beta )))\geq K_{1}(\alpha ).\\&&&{\text{For all }}\alpha :K_{1}(\alpha )\leq K_{1}(J((i,\alpha ,\beta )))=\alpha .\\&&&{\text{For all }}\alpha \notin Rng(J_{0}):i>0\land K_{1}(\alpha )\leq K_{1}(J((0,\alpha ,\beta )))<K_{1}(J((i,\alpha ,\beta )))=\alpha .\\&&&{\text{Similarly for }}K_{2}(\alpha ).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&{\text{The following definitions are for subscripts }}\,i\,{\text{ in }}\,J_{i},\,{\mathfrak {F}}_{i}(X,Y),\,q_{i}{\text{ and }}\,Q_{i}.\\&&&p=1\;\,\quad {\text{// Pair}}\\&&&e=2\;\,\quad {\text{// Epsilon}}\\&&&m=3\quad {\text{// Minus for set minus (set difference)}}\\&&&v=4\;\,\quad {\text{// Product by V}}\\&&&d=5\;\,\quad {\text{// Domain}}\\&&&t=6\;\,\quad {\text{// Transposition}}\\&&&c=7\;\,\quad {\text{// Circular permutation}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\text{Define the element functions: }}\;&&q_{5}=q_{d}=dom\;{\text{ where }}dom((y,x))=x\land dom\,{\mathfrak {Fn}}\,V^{2}.\\&&&q_{6}=q_{t}=trans\;{\text{ where }}tr((x,y,z))=(y,x,z)\land tr\,{\mathfrak {Fn}}\,V^{3}.\\&&&q_{7}=q_{c}=cp\;{\text{ where }}cp((x,y,z))=(z,x,y)\land cp\,{\mathfrak {Fn}}\,V^{3}.\\&&&tr_{2}((x,y)=(y,x)\land tr_{2}\,{\mathfrak {Fn}}\,V^{2}.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\text{Define the class functions: }}\;&&Q_{5}=Q_{d}=Dom\;{\text{ where }}Dom(X)=dom[X].\\&&&Q_{6}=Q_{t}=Tr\;{\text{ where }}Tr(X)=tr[X].\\&&&Q_{7}=Q_{c}=Cp\;{\text{ where }}Cp(X)=cp[X].\\&&&Q_{4}=Q_{v}=Pv\;{\text{ where }}Pv(X)=dom^{-1}[X]=V\times X.\\&&&{\text{NOTE: }}\;dom^{-1}{\text{ refers to inverse of the relation }}dom.\\&&&Tr_{2}(X)=tr_{2}[X].\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\text{Define the set construction operators: }}\;\;&&{\mathfrak {F}}_{1}(X,Y)={\mathfrak {F}}_{p}(X,Y)=\{X,Y\},\\&&&{\mathfrak {F}}_{2}(X,Y)={\mathfrak {F}}_{e}(X,Y)=E\cap X,\\&&&{\mathfrak {F}}_{3}(X,Y)={\mathfrak {F}}_{m}(X,Y)=X\setminus Y,\\&&&{\mathfrak {F}}_{4}(X,Y)={\mathfrak {F}}_{v}(X,Y)=X\cap Pv(Y),\;\;\;\;\quad {\text{// Product by V}}\\&&&{\mathfrak {F}}_{5}(X,Y)={\mathfrak {F}}_{d}(X,Y)=X\cap Dom(Y),\quad {\text{// Domain}}\\&&&{\mathfrak {F}}_{6}(X,Y)={\mathfrak {F}}_{t}(X,Y)=X\cap Tr(Y),\;\;\;\;\quad {\text{// Transposition}}\\&&&{\mathfrak {F}}_{7}(X,Y)={\mathfrak {F}}_{c}(X,Y)=X\cap Cp(Y),\;\;\;\quad {\text{// Circular permutation}}\\\\\end{alignedat}}$

${\text{In the following, }}1\leq i\leq 7.$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&\alpha \in Rng(J_{0})\implies F(\alpha )=Rng(F\upharpoonright \alpha ),\\&&&\alpha \in Rng(J_{i})\implies F(\alpha )={\mathfrak {F}}_{i}(F(K_{1}(\alpha )),F(K_{2}(\alpha ))),\\&&&F\,Fn\,On.\\\\&{\textbf {Theorem.}}&&{\text{The function }}F{\text{ exists.}}\\&{\textbf {Proof.}}&&{\text{By transfinite recursion. Define the function }}G\subseteq V^{2}:\\&&&(x,y)\in G\iff Dom(x)\in Rng(J_{0})\implies y=Rng(x),\\&&&\qquad \qquad \;\;\iff Dom(x)\in Rng(J_{i})\implies y={\mathfrak {F}}_{i}(x(K_{1}(Dom(x)),\,x(K_{2}(Dom(x))),\\&&&\qquad \qquad \;\;\iff {\text{otherwise, }}y=\emptyset .\\&&&{\text{So by transfinite recursion, the function }}F=G(F\upharpoonright \alpha ){\text{ exists.}}\\&&&{\text{We now prove this function is the function in the above definition.}}\\&&&{\text{We have }}Dom(x)=Dom(F\upharpoonright \alpha )=\alpha .\\&&&{\text{Since }}i>0,{\text{ for }}\alpha \in Rng(J_{i}),K_{1}(Dom(x))=K_{1}(\alpha )<\alpha {\text{ and }}K_{2}(Dom(x))=K_{2}(\alpha )<\alpha .\\&&&{\text{This implies }}x(K_{1}(Dom(x))=F\upharpoonright \alpha (K_{1}(\alpha ))=F(K_{1}(\alpha )){\text{ and similarly for }}x(K_{2}(Dom(x)).\\&&&\therefore \;\;\alpha \in Rng(J_{0})\implies F(\alpha )=Rng(F\upharpoonright \alpha ),\\&&&\quad \;\;\alpha \in Rng(J_{i})\implies F(\alpha )={\mathfrak {F}}_{i}(F(K_{1}(\alpha )),F(K_{2}(\alpha ))).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&F(J_{i}(\alpha ,\beta ))={\mathfrak {F}}_{i}(K_{1}(\alpha ),K_{2}(\beta )).\\&{\textbf {Proof.}}&&{\text{From last theorem: }}\;F(J_{i}(\alpha ,\beta ))={\mathfrak {F}}_{i}(F(K_{1}(J_{i}(\alpha ,\beta ))),F(K_{2}(J_{i}(\alpha ,\beta ))))\\&&&\qquad \qquad \qquad \qquad \qquad \qquad \qquad ={\mathfrak {F}}_{i}(F(\alpha ),F(\beta )).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&F(J_{0}(\alpha ,\beta ))=Rng(F\upharpoonright J_{0}(\alpha ,\beta )),\\&&&F(J_{1}(\alpha ,\beta ))=\{F(\alpha ),F(\beta )\},\\&&&F(J_{2}(\alpha ,\beta ))=E\cap F(\alpha ),\\&&&F(J_{3}(\alpha ,\beta ))=F(\alpha )\setminus F(\beta ),\\&&&F(J_{4}(\alpha ,\beta ))=F(\alpha )\cap Dom(F(\beta )),\\&&&F(J_{5}(\alpha ,\beta ))=F(\alpha )\cap Pv(F(\beta )),\\&&&F(J_{6}(\alpha ,\beta ))=F(\alpha )\cap Cp(F(\beta )),\\&&&F(J_{7}(\alpha ,\beta ))=F(\alpha )\cap Tr(F(\beta )),\\&{\textbf {Proof.}}&&{\text{Use last theorem and definition of }}{\mathfrak {F}}_{i}(X,Y).\\\\&{\textbf {Definition.}}\;\;&&L=Rng(F).\\\end{alignedat}}$

Program: input x ∈ F(γ), output x = F(δ)

$\mathbf {function} \;{\text{ordinal}}(x,\,\gamma )$
${\begin{aligned}\mathbf {input} :\;&x{\text{ is a set.}}\\&\gamma {\text{ is an ordinal such that }}x\in F(\gamma ).\\\;\;\;\;\mathbf {output} :\;&{\text{ordinal }}\delta {\text{ that satisfies: }}x=F(\delta )\land \delta <\gamma .\end{aligned}}$

$\mathbf {begin}$

$\gamma =J(i,\alpha ,\beta );$

$\mathbf {case} \;i\;\mathbf {of}$

${\begin{alignedat}{2}\qquad \quad \;&0:\;\mathbf {if} \;(x=F(\delta )\land \delta <\gamma )\quad {\text{ // }}x\in F(\gamma )=Rng(F\upharpoonright \gamma ){\text{ implies }}\exists \delta \,(\delta <\gamma \land x=F(\delta )).\\&\qquad \quad \,\mathbf {return} \;\delta ;\\&1:\;\mathbf {if} \;x=F(\alpha )\qquad \qquad \quad {\text{ // }}\alpha ,\beta <\gamma .{\text{ Also, }}x\in F(\gamma )=\{F(\alpha ),F(\beta )\}{\text{ implies }}x=F(\alpha )\lor x=F(\beta ).\\&\qquad \quad \,\mathbf {return} \;\alpha ;\\&\quad \;\;\mathbf {else} \;\mathbf {if} \;x=F(\beta )\\&\qquad \quad \,\mathbf {return} \;\beta ;\\&2,3,4,5,6,7:\qquad \qquad \quad \;\;{\text{ // For some class }}Y\!:x\in F(\gamma )=F(\alpha )\cap Y,{\text{ so }}x\in F(\alpha )\land \alpha <\gamma .\\&\qquad \quad \,\mathbf {return} \;{\text{ordinal}}(x,\,\alpha );\\\end{alignedat}}$

$\mathbf {end}$

$\mathbf {end}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}&&{\text{ Function ordinal}}(x,\,\gamma ){\text{ terminates and returns }}{\text{ordinal }}\delta {\text{ that satisfies: }}\delta <\gamma \land x=F(\delta ).\\&{\textbf {Proof.}}&&{\text{All cases except the }}2,3,4,5,6,7{\text{ terminate and return an ordinal less than the argument }}\gamma .\\&&&{\text{This case does a recursive call with an argument less than }}\gamma .{\text{ If the function does not terminate,}}\\&&&{\text{it is because this case always occurs. This produces an infinite decreasing sequence of ordinals: }}\\&&&\gamma >\gamma _{1}>\cdots >\gamma _{n}>\cdots .{\text{ This contradicts the fact that there is no such decreasing sequence of ordinals.}}\\&&&\therefore \;{\text{ The function terminates in one of the other cases and returns a }}\delta {\text{ that satisfies: }}\delta <\gamma \land x=F(\delta ).\\\\\end{alignedat}}$

Theorems about L

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;&&{\mathfrak {L}}(A)\iff A\subseteq L\land \forall x(x\in L\implies A\cap x\in L).\\&&&{\text{That is, a class is constructible if and only if its members are constructible}}\\&&&{\text{and the intersection with any constructible set is constructible.}}\\&{\textbf {Definition.}}&&{\bar {x}},\dots ,{\bar {z}}{\text{ will be used as variables for constructible sets and }}\\&&&{\bar {X}},\dots ,{\bar {Z}}{\text{ will be used as variables for constructible classes.}}\\&{\textbf {Definition.}}&&{\text{The order of set }}x{\text{ is the smallest ordinal }}\alpha {\text{ such that }}x=F(\alpha ).\\&&&(x,\alpha )\in Od\iff (x,\alpha )\in F\land \forall \beta (\beta \in \alpha \implies (x,\beta )\notin F)\land Od\subseteq V^{2}.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&x\in F(\alpha )\implies \exists \beta \,(\beta <\alpha \land x=F(\beta )).\\&{\textbf {Proof.}}&&{\text{See program and theorem of last section.}}\\\\&{\textbf {Theorem.}}\;\;&&Trans(F[\alpha ]).\\&{\textbf {Proof.}}&&{\text{Let }}x\in y\in F[\alpha ].{\text{ Then }}x\in y=F(\beta ){\text{ where }}\beta <\alpha .\\&&&{\text{So }}x\in F(\beta ).{\text{ By the theorem above: }}\,\exists \delta \,(\delta <\beta <\alpha \land x=F(\delta )).\;\;\therefore x\in F[\alpha ].\\\\&{\textbf {Theorem.}}\;\;&&Trans(L).\\&{\textbf {Proof.}}&&{\text{Let }}x\in y\in L.{\text{ Then }}y=F(\alpha ){\text{ for some }}\alpha .\\&&&{\text{So }}x\in F(\alpha ).{\text{ By the theorem above: }}\,\exists \beta \,(x=F(\beta )).\;\;\therefore x\in L.\\\\&{\textbf {Theorem.}}&&x\in y\land x,y\in L\implies Od(x)<Od(y).{\text{ In other words, }}x\in F[\alpha ]\implies Od(x)<\alpha .\\&{\textbf {Proof.}}&&{\text{Let }}Od(y)=\alpha .{\text{ Then }}x\in F(\alpha ),{\text{ so }}\exists \beta \,(\beta <\alpha \land x=F(\beta )).\\&&&\therefore Od(x)\leq \beta <\alpha =Od(y).\\\\&{\textbf {Theorem.}}&&{\mathfrak {F_{i}}}({\bar {x}},{\bar {y}})\in L.\\&{\textbf {Proof.}}&&{\bar {x}}=F(\alpha ),{\bar {y}}=F(\beta )\implies F(J_{i}(\alpha ,\beta ))={\mathfrak {F_{i}}}({\bar {x}},{\bar {y}}).\\\\&{\textbf {Theorem.}}&&{\bar {x}}\cap {\bar {y}}\in L.\\&{\textbf {Proof.}}&&{\bar {x}}\cap {\bar {y}}={\bar {x}}\setminus ({\bar {x}}\setminus {\bar {y}})={\mathfrak {F_{3}}}({\bar {x}},{\mathfrak {F_{3}}}({\bar {x}},{\bar {y}})).\\\\&{\textbf {Theorem.}}&&x,y\in L\iff (x,y)\in L{\text{ and }}\;x,y,z\in L\iff (x,y,z)\in L.\\&{\textbf {Proof.}}&&x,y\in L\land (x,y)=\{\{x\},\{x,y\}\}\implies (x,y)={\mathfrak {F_{1}}}(x,{\mathfrak {F_{1}}}(x,y)).\\&&&(x,y)\in L\land (x,y)=\{\{x\},\{x,y\}\}\implies \{x,y\}\in L\implies x,y\in L.{\text{ Or use }}Trans(L).\\&&&{\text{By induction, true for }}n{\text{-tuples.}}\\\\&{\textbf {Theorem.}}&&(x,y)\in L\iff (y,x)\in L{\text{ and }}\;(x,y,z)\in L\iff (z,x,y)\in L\iff (x,z,y)\in L.\\&{\textbf {Proof.}}&&{\text{By last theorem}}.\\\\&{\textbf {Theorem.}}&&dom({\bar {x}}),tr({\bar {x}}),cp({\bar {x}}),tr_{2}({\bar {x}})\in L.\\&{\textbf {Proof.}}&&{\text{By last two theorems}}.\\&&&{\text{For example, }}{\bar {x}}=(u,v,w)\implies u,v,w\in L\implies tr({\bar {x}})=(u,w,v)\in L.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;\;&&x\subseteq L\implies \exists {\bar {y}}(x\subseteq {\bar {y}}).\\&{\textbf {Proof.}}&&{\text{Let }}\alpha =least\,(On\setminus \{\beta :\exists u(u\in x\land \beta =Od(u)\}).\\&&&{\text{Then }}{\bar {y}}=F(J_{0}(\alpha ,0))=Rng(F\upharpoonright \alpha ){\text{ satisfies theorem.}}\\\\&{\textbf {Theorem.}}&&{\mathfrak {M}}({\bar {X}})\implies {\bar {X}}\in L.\\&{\textbf {Proof.}}&&{\mathfrak {L}}({\bar {X}})\implies {\bar {X}}\subseteq L.\;\;{\mathfrak {M}}({\bar {X}}){\text{ and last theorem imply }}\exists {\bar {y}}({\bar {X}}\subseteq {\bar {y}}).\\&&&{\mathfrak {L}}({\bar {X}})\implies {\bar {X}}={\bar {X}}\cap {\bar {y}}\in L.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {x}}).\\&{\textbf {Proof.}}&&{\bar {x}}\subseteq L.\;{\bar {x}}\cap {\bar {y}}\in L.\\\\&{\textbf {Theorem.}}&&{\bar {x}}\cup {\bar {y}}\in L.\\&{\textbf {Proof.}}&&{\bar {x}}\cup {\bar {y}}\subseteq L\implies \exists {\bar {z}}({\bar {x}}\cup {\bar {y}}\subseteq {\bar {z}}).\\&&&{\bar {x}}\cup {\bar {y}}=({\bar {x}}^{c({\bar {z}})}\cap {\bar {y}}^{c({\bar {z}})})^{c({\bar {z}})}={\bar {z}}\setminus (({\bar {z}}\setminus {\bar {x}})\cap ({\bar {z}}\setminus {\bar {y}})).\\&&&{\text{Gödel used: }}\;{\bar {x}}\cup {\bar {y}}={\bar {z}}\setminus (({\bar {z}}\setminus {\bar {x}})\setminus {\bar {y}}).\\\\&{\textbf {Theorem.}}&&\emptyset \in L{\text{ or }}0\in L.\\&{\textbf {Proof.}}&&F(J_{0}(0,0))=Rng(F\upharpoonright 0)=\emptyset .\;{\text{Gödel used: }}\;{\bar {x}}\setminus {\bar {x}}=\emptyset .\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}(L).\\&{\textbf {Proof.}}&&L\subseteq L.\;L\cap {\bar {x}}={\bar {x}}\in L.\\\end{alignedat}}$

Theorems about L (section 2)

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&{\mathfrak {L}}(E\cap L).\\&{\textbf {Proof.}}&&E\cap L\subseteq L.\\&&&{\text{Let }}{\bar {x}}=F(\alpha ).{\text{ Then }}(E\cap L)\cap {\bar {x}}=E\cap F(\alpha )=F(J_{2}(\alpha ,0))\in L.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {A}}\setminus {\bar {B}}).\\&{\textbf {Proof.}}&&{\bar {A}}\setminus {\bar {B}}\subseteq {\bar {A}}\subseteq L.\\&&&({\bar {A}}\setminus {\bar {B}})\cap {\bar {x}}=({\bar {A}}\cap {\bar {x}})\setminus ({\bar {B}}\cap {\bar {x}})={\bar {y}}\setminus {\bar {z}}\in L.\\&&&{\text{The last expression is the difference of two constructible sets, which is constructible by }}{\mathfrak {F_{3}}}.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {A}}\cap {\bar {B}}).\\&{\textbf {Proof.}}&&{\bar {A}}\cap {\bar {B}}\subseteq {\bar {A}}\subseteq L.\\&&&({\bar {A}}\cap {\bar {B}})\cap {\bar {x}}={\bar {A}}\cap ({\bar {B}}\cap {\bar {x}})={\bar {A}}\cap {\bar {y}}\in L.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {A}}\cup {\bar {B}}).\\&{\textbf {Proof.}}&&{\bar {A}}\cup {\bar {B}}\subseteq L.\\&&&({\bar {A}}\cup {\bar {B}})\cap {\bar {x}}=({\bar {B}}\cap {\bar {x}})\cup ({\bar {A}}\cap {\bar {x}})={\bar {y}}\cup {\bar {z}}\in L.\\\\&{\textbf {Theorem.}}&&Dom({\bar {x}})\in L;\;Tr({\bar {x}})\in L;\;Cp({\bar {x}})\in L.\\&{\textbf {Proof.}}&&{\text{Let }}i=d,t,{\text{ or }}c.\;Q_{i}({\bar {x}}){\text{ is a set by replacement}}.\;\,\therefore \exists {\bar {y}}(Q_{i}({\bar {x}})\subseteq {\bar {y}}).\\&&&{\text{Let }}F(\alpha )={\bar {y}};F(\beta )={\bar {x}}.{\text{ Then }}F(J_{i}(\alpha ,\beta ))=F(\alpha )\cap Q_{i}(F(\beta ))={\bar {y}}\cap Q_{i}({\bar {x}})=Q_{i}({\bar {x}}).\\&&&\therefore Q_{i}({\bar {x}})\in L.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Tr_{2}({\bar {x}})\in L.\\&{\textbf {Proof.}}\;\;Tr_{2}({\bar {x}})=Dom(Tr(L\cap Pv({\bar {x}}))):\\&y\in Dom(Tr(L\cap Pv({\bar {x}})))\iff \exists u,v,y_{2},y_{3},w(y=(v,u)\land y_{2}=(w,v,u)\land y_{3}=(w,u,v)\land w\in L\land (u,v)\in {\bar {x}})\\&\qquad \qquad \qquad \qquad \qquad \quad \implies y\in Tr_{2}({\bar {x}}).\\&y\in Tr_{2}({\bar {x}})\iff \exists u,v(y=(v,u)\land (u,v)\in {\bar {x}}))\\&\qquad \qquad \quad \implies \exists u,v,y_{2},y_{3},w(y=(v,u)\land w\in L\land y_{3}=(w,u,v)\land y_{2}=(w,v,u)\land (u,v)\in {\bar {x}})\\&\qquad \qquad \quad \iff y\in Dom(Tr(L\cap Pv({\bar {x}})).\\\\&{\textbf {Theorem.}}&&Rng({\bar {x}})\in L.\\&{\textbf {Proof.}}\;\;Rng({\bar {x}})=Dom(Tr2({\bar {x}})):\\\\\\\end{alignedat}}$

Theorems about L (section 3)

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&{\mathfrak {L}}(Dom({\bar {A}}));\;{\mathfrak {L}}(Tr({\bar {A}}));\;{\mathfrak {L}}(Cp({\bar {A}})).\\&{\textbf {Proof.}}&&{\text{Let }}i=d,t,{\text{ or }}c.\;\,Q_{i}({\bar {A}})\subseteq L:v\in Q_{i}({\bar {A}})\implies \exists u\,(v=q_{i}(u)\land u\in {\bar {A}}\subseteq L).\\&&&{\text{From a previous theorem: }}u\in L\implies q_{i}(u)=v\in L.\;\,\therefore Q_{i}({\bar {A}})\subseteq L.\\&&&Q_{i}({\bar {A}})\cap {\bar {x}}\in L:\;\,{\text{Strategy: Find a }}{\bar {z}}{\text{ such that }}Q_{i}({\bar {z}})\cap {\bar {x}}=Q_{i}({\bar {A}})\cap {\bar {x}}.\\&&&{\text{Then }}Q_{i}({\bar {z}})\cap {\bar {x}}\in L{\text{ since }}F(J(i,\alpha ,\beta )={\mathfrak {F}}_{i}(F(\alpha ),F(\beta ))={\bar {x}}\cap Q_{i}({\bar {z}}).\\&&&{\text{For }}v\in Q_{i}({\bar {A}})\cap {\bar {x}},{\text{ let }}\alpha _{v}=least\,\{\alpha :u\in {\bar {A}}\land v=q_{i}(u)\land u=F(\alpha )\}.\\&&&{\text{Let }}y=\{F(\alpha _{v}):v\in {\bar {x}}\},{\text{ which is a set by replacement.}}\\&&&{\text{Let }}\exists {\bar {b}}(y\subseteq {\bar {b}}).\;{\text{Let }}{\bar {z}}={\bar {A}}\cap {\bar {b}}.\;{\text{Then }}y\subseteq {\bar {z}}\subseteq {\bar {A}}.\\&&&{\bar {z}}\subseteq {\bar {A}}\implies Q_{i}({\bar {z}})\cap {\bar {x}}\subseteq Q_{i}({\bar {A}})\cap {\bar {x}}.\\&&&v\in Q_{i}({\bar {A}})\cap {\bar {x}}\implies \exists u(u\in {\bar {A}}\land v=q_{i}(u))\\&&&\qquad \qquad \qquad \;\,\implies u=F(\alpha _{v})\implies u\in y\implies u\in {\bar {z}}\implies v\in Q({\bar {z}}).\\&&&{\text{Hence, }}v\in Q_{i}({\bar {z}})\cap {\bar {x}}.\,{\text{ So }}Q_{i}({\bar {A}})\cap {\bar {x}}\subseteq Q({\bar {z}})\cap {\bar {x}}.\\&&&\therefore Q_{i}({\bar {A}})\cap {\bar {x}}=Q_{i}({\bar {z}})\cap {\bar {x}}\in L.\\\\&{\textbf {Theorem.}}&&L\cap (V\times {\bar {A}})=L\times {\bar {A}}.\\&{\textbf {Proof.}}&&x\in L\cap (V\times {\bar {A}})\iff x\in L\land x=(u,v)\land u\in V\land v\in {\bar {A}}.\\&&&\qquad \qquad \qquad \quad \;\,\iff x=(u,v)\land u,v\in L\land v\in {\bar {A}}\\&&&\qquad \qquad \qquad \quad \;\,\iff x=(u,v)\land u\in L\land v\in {\bar {A}}\\&&&\qquad \qquad \qquad \quad \;\,\iff x\in L\times {\bar {A}}.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}(L\cap Pv({\bar {A}})){\text{ or }}{\mathfrak {L}}(L\cap (V\times {\bar {A}})){\text{ or }}{\mathfrak {L}}(L\times {\bar {A}})).\\&{\textbf {Proof.}}&&L\cap Pv({\bar {A}})\subseteq L.\\&&&(L\cap Pv({\bar {A}}))\cap {\bar {x}}\in L:{\text{In last proof: replace }}Q_{i}({\bar {A}}){\text{ with }}L\cap Pv({\bar {A}}).\\&&&(L\cap Pv({\bar {A}}))\cap {\bar {x}}\in L:\;\,{\text{Strategy: Find a }}{\bar {z}}{\text{ such that }}Pv({\bar {z}})\cap {\bar {x}}=(L\cap Pv({\bar {A}}))\cap {\bar {x}}.\\&&&{\text{Then }}Pv({\bar {z}})\cap {\bar {x}}\in L{\text{ since }}F(J(v,\alpha ,\beta )={\mathfrak {F}}_{v}(F(\alpha ),F(\beta ))={\bar {x}}\cap Pv({\bar {z}}).\\&&&{\text{For }}v\in (L\cap Pv({\bar {A}}))\cap {\bar {x}},{\text{ let }}\alpha _{v}=least\,\{\alpha :u\in {\bar {A}}\land \exists w(v=(w,u)\land u=F(\alpha )\}.\\&&&{\text{Let }}y=\{F(\alpha _{v}):v\in {\bar {x}}\},{\text{ which is a set by replacement.}}\\&&&{\text{Let }}\exists {\bar {b}}(y\subseteq {\bar {b}}).\;{\text{Let }}{\bar {z}}=(L\cap Pv({\bar {A}}))\cap {\bar {b}}.\;{\text{Then }}y\subseteq {\bar {z}}\subseteq (L\cap Pv({\bar {A}})).\\&&&{\bar {z}}\subseteq (L\cap Pv({\bar {A}}))\implies Q_{i}({\bar {z}})\cap {\bar {x}}\subseteq (L\cap Pv({\bar {A}}))\cap {\bar {x}}.\\&&&v\in (L\cap Pv({\bar {A}}))\cap {\bar {x}}\implies \exists u(u\in {\bar {A}}\land \exists w(v=(w,u))).\\&&&\qquad \qquad \qquad \qquad \quad \implies u=F(\alpha _{v})\implies u\in y\implies u\in {\bar {z}}\implies v\in Q({\bar {z}}).\\&&&{\text{Hence, }}v\in Pv({\bar {z}})\cap {\bar {x}}.\,{\text{ So }}(L\cap Pv({\bar {A}}))\cap {\bar {x}}\subseteq Q({\bar {z}})\cap {\bar {x}}.\\&&&\therefore (L\cap Pv({\bar {A}}))\cap {\bar {x}}=Pv({\bar {z}})\cap {\bar {x}}\in L.\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}(Tr_{2}({\bar {A}})).\\&{\textbf {Proof.}}&&Tr_{2}({\bar {A}})=Dom(Tr(L\cap Pv({\bar {A}}))).\\&&&{\mathfrak {L}}(L\cap Pv({\bar {A}}))\implies {\mathfrak {L}}(Tr(L\cap Pv({\bar {A}}))\\&&&\qquad \qquad \qquad \;\implies {\mathfrak {L}}(Dom(Tr(L\cap Pv({\bar {A}})))\\&&&\qquad \qquad \qquad \;\implies {\mathfrak {L}}(Tr_{2}({\bar {A}})).\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {A}}\times {\bar {B}}).\\&{\textbf {Proof.}}&&({\bar {A}}\times L)\cap (L\times {\bar {B}})=({\bar {A}}\cap L)\times (L\cap {\bar {B}})={\bar {A}}\times {\bar {B}}.\\&&&{\text{By a previous theorem: }}{\mathfrak {L}}(L\times {\bar {B}}).\\&&&{\text{Now }}{\bar {A}}\times L=Tr_{2}(L\times {\bar {A}})\implies {\mathfrak {L}}({\bar {A}}\times L).\\&&&\therefore \;{\mathfrak {L}}(({\bar {A}}\times L)\cap (L\times {\bar {B}})){\text{ or }}{\mathfrak {L}}({\bar {A}}\times {\bar {B}}).\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}(Rng({\bar {A}})).\\&{\textbf {Proof.}}&&Rng(({\bar {A}})=Dom(Tr_{2}(({\bar {A}})))\,{\text{ so result follows from: }}\,{\mathfrak {L}}(Tr_{2}({\bar {A}})),\,{\mathfrak {L}}(Dom({\bar {A}})).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&{\mathfrak {L}}({\bar {A}}\upharpoonright {\bar {B}}).\\&{\textbf {Proof.}}&&{\bar {A}}\upharpoonright {\bar {B}}={\bar {A}}\cap (V\times {\bar {B}})={\bar {A}}\cap L\cap (V\times {\bar {B}})={\bar {A}}\cap (L\times {\bar {B}}),\\&&&{\text{ so result follows from: }}\,{\mathfrak {L}}(L\times {\bar {B}}),\,{\mathfrak {L}}({\bar {A}}\cap {\bar {B}}).\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}({\bar {A}}[{\bar {B}}]).\\&{\textbf {Proof.}}&&{\bar {A}}[{\bar {B}}]=Rng({\bar {A}}\upharpoonright {\bar {B}})\,{\text{ so result follows from: }}\,{\mathfrak {L}}({\bar {A}}\upharpoonright {\bar {B}}),\,{\mathfrak {L}}(Rng({\bar {A}})).\\\\&{\textbf {Theorem.}}&&{\mathfrak {L}}(\{{\bar {X}},{\bar {Y}}\}).\\&{\textbf {Proof.}}&&{\text{By definition of ordered pair for classes: }}\{{\bar {X}},{\bar {Y}}\}=\emptyset ,\{{\bar {X}}\},\{{\bar {Y}}\},{\text{ or }}\{{\bar {X}},{\bar {Y}}\}\\&&&{\text{where only sets appear in braces. Theorem follows from preceding theorems.}}\\\\\end{alignedat}}$

Theorems for proving absoluteness

${\begin{alignedat}{2}&{\textbf {Absoluteness}}\;{\textbf {theorems.}}\;\;{\text{These theorems are used to prove absoluteness.}}\\&Abs_{1}{\text{:}}\;{\bigl [}\,\forall u(P(u)\implies Q(u))\land (P(u)\implies u\in L)\,{\bigr ]}\iff \forall {\bar {u}}(P({\bar {u}})\implies Q({\bar {u}})).\\&Abs_{2}{\text{:}}\;{\bigl [}\,\forall u(P(u)\iff Q(u))\land (P(u)\implies u\in L)\land (Q(u)\implies u\in L)\,{\bigr ]}\iff \forall {\bar {u}}(P({\bar {u}})\iff Q({\bar {u}})).\\&Abs_{3}{\text{:}}\;{\bigl [}\,\forall u\,\forall v\,\forall w(P(u,v,w)\implies Q(u,v,w))\land (P(u,v,w)\implies u,v,w\in L)\,{\bigr ]}\\&\qquad \;\iff \forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}(P({\bar {u}},{\bar {v}},{\bar {w}})\implies Q({\bar {u}},{\bar {v}},{\bar {w}})).\\&{\textbf {Proof.}}\;\;\Longrightarrow {\text{direction:}}\\&\quad \forall u(P(u)\implies Q(u))\implies \forall u(u\in L\implies (P(u)\implies Q(u)))\iff \forall {\bar {u}}(P({\bar {u}})\implies Q({\bar {u}})).\\&\quad \forall u(P(u)\iff Q(u))\implies \forall u(u\in L\implies (P(u)\iff Q(u)))\iff \forall {\bar {u}}(P({\bar {u}})\iff Q({\bar {u}})).\\&\Longleftarrow {\text{direction:}}\\&{\text{Case 1: }}\;\;u\in L.\\&\quad \forall {\bar {u}}(P({\bar {u}})\implies Q({\bar {u}}))\iff \forall u(u\in L\implies (P(u)\implies Q(u))),{\text{ so }}u\in L{\text{ implies }}P(u)\implies Q(u).\\&\quad \forall {\bar {u}}(P({\bar {u}})\iff Q({\bar {u}}))\iff \forall u(u\in L\implies (P(u)\iff Q(u))),{\text{ so }}u\in L{\text{ implies }}P(u)\iff Q(u).\\&{\text{Case 2: }}\;\;u\notin L.\\&\quad \forall u(u\notin L\implies \neg P(u)),{\text{ so }}u\notin L{\text{ implies }}P(u)\implies Q(u).\\&\quad \forall u(u\notin L\implies \neg P(u)\land \neg Q(u)),{\text{ so }}u\notin L{\text{ implies }}P(u)\iff Q(u).\\&{\text{Putting both cases together: }}\\&\quad \forall {\bar {u}}(P({\bar {u}})\implies Q({\bar {u}}))\implies \forall u(P(u)\implies Q(u)).\\&\quad \forall {\bar {u}}(P({\bar {u}})\iff Q({\bar {u}}))\implies \forall u(P(u)\iff Q(u)).\\\\\end{alignedat}}$

Absoluteness

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&{\bar {X}}\subseteq {\bar {Y}}\iff {\bar {X}}\subseteq _{l}{\bar {Y}}.\\&{\textbf {Proof.}}&&\!{\bar {X}}\subseteq _{l}{\bar {Y}}\iff \forall {\bar {u}}({\bar {u}}\in {\bar {X}}\implies {\bar {u}}\in {\bar {Y}}).\\&&&{\bar {X}}\subseteq {\bar {Y}}\iff \forall u(u\in {\bar {X}}\implies u\in {\bar {Y}})\\&&&\qquad \quad \,\iff \forall {\bar {u}}({\bar {u}}\in {\bar {X}}\implies {\bar {u}}\in {\bar {Y}}){\text{ by }}Abs_{1}{\text{ since }}u\in {\bar {X}}\implies u\in L.\\&&&\qquad \quad \;\iff {\bar {X}}\subseteq _{l}{\bar {Y}}.\\\\&{\textbf {Theorem.}}&&{\bar {X}}={\bar {Y}}\iff \forall {\bar {u}}({\bar {u}}\in {\bar {X}}\iff {\bar {u}}\in {\bar {Y}}).\\&&&{\text{Constructive extensionality:}}\\&&&\quad {\text{Two constructive classes are equal iff they have the same constructible elements.}}\\&{\textbf {Proof.}}&&{\bar {X}}={\bar {Y}}\iff \forall u(u\in {\bar {X}}\iff u\in {\bar {Y}})\\&&&\qquad \quad \;\iff \forall {\bar {u}}({\bar {u}}\in {\bar {X}}\implies {\bar {u}}\in {\bar {Y}}){\text{ by }}Abs_{2}{\text{ since }}u\in {\bar {X}}{\text{ and }}u\in {\bar {Y}}\implies u\in L.\\\\&{\textbf {Theorem.}}&&\{{\bar {X}},{\bar {Y}}\}_{l}=\{{\bar {X}},{\bar {Y}}\}.\\&{\textbf {Proof.}}&&\forall {\bar {u}}({\bar {u}}\in \{{\bar {X}},{\bar {Y}}\}_{l}\iff {\bar {u}}={\bar {X}}\lor {\bar {u}}={\bar {Y}}).\\&&&{\text{A previous theorem proved that }}\{{\bar {X}},{\bar {Y}}\}\in L.\\&&&{\text{Using }}Abs_{2}{\text{ since }}u\in \{{\bar {X}},{\bar {Y}}\}\implies u\in L{\text{ and }}u={\bar {X}}\lor u={\bar {Y}}\implies u\in L:\\&&&\forall u(u\in \{{\bar {X}},{\bar {Y}}\}\iff u={\bar {X}}\lor u={\bar {Y}})\iff \forall {\bar {u}}({\bar {u}}\in \{{\bar {X}},{\bar {Y}}\}\iff {\bar {u}}={\bar {X}}\lor {\bar {u}}={\bar {Y}}),\\&&&\therefore \;\{{\bar {X}},{\bar {Y}}\}_{l}=\{{\bar {X}},{\bar {Y}}\}{\text{ by constructive extensionality.}}\\\\&{\textbf {Theorem.}}&&{\text{If }}A,B{\text{ are absolute, then }}A_{l}(B_{l}({\bar {X}}))=A(B({\bar {X}})).\\&{\textbf {Proof.}}&&{\text{Since }}A{\text{ is absolute and }}B_{l}({\bar {X}}){\text{ is constructive, and }}B{\text{ is absolute:}}\\&&&\qquad A_{l}(B_{l}({\bar {X}}))=A(B_{l}({\bar {X}}))=A(B({\bar {X}})).\\\\&{\textbf {Theorem.}}&&({\bar {X}},{\bar {Y}})_{l}=({\bar {X}},{\bar {Y}}).\;{\text{ (An example of last proof.)}}\\&{\textbf {Proof.}}&&({\bar {X}},{\bar {Y}})_{l}=\{\{{\bar {X}}\}_{l},\{{\bar {X}},{\bar {Y}}\}_{l}\}_{l}=\{\{{\bar {X}}\}_{l},\{{\bar {X}},{\bar {Y}}\}_{l}\}=\{\{{\bar {X}}\},\{{\bar {X}},{\bar {Y}}\}\}=({\bar {X}},{\bar {Y}}).\\\\&{\textbf {Theorem.}}&&{\text{If }}_{n}A,\,\ldots ,\,_{1}A{\text{ are absolute, then }}_{n}A_{l}(\cdots (_{1}A_{l}({\bar {X}}))\,=\,_{n}A(\cdots (_{1}A({\bar {X}})).\\&{\textbf {Proof.}}&&{\text{Basis step:}}\;_{1}A_{l}({\bar {X}})=\,_{1}A({\bar {X}}).\\&&&{\text{Inductive step: Assume }}\;_{n}A_{l}(\cdots (_{1}A_{l}({\bar {X}}))\,=\,_{n}A(\cdots (_{1}A({\bar {X}})).\\&&&{\text{Then: }}\;_{n+1}A_{l}(_{n}A_{l}(\cdots (_{1}A_{l}({\bar {X}})))\,=\,_{n+1}A(_{n}A_{l}(\cdots (_{1}A_{l}({\bar {X}})))\,=\,_{n+1}A(_{n}A(\cdots (_{1}A({\bar {X}}))).\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;&&{\mathfrak {M}}_{l}({\bar {X}})\iff {\mathfrak {M}}({\bar {X}}).\\&{\textbf {Proof.}}&&{\mathfrak {M}}_{l}({\bar {X}})\iff {\bar {X}}\in L.\\&&&{\bar {X}}\in L\implies {\mathfrak {M}}({\bar {X}}){\text{ by axiom A2. }}\;{\mathfrak {M}}({\bar {X}})\implies {\bar {X}}\in L{\text{ by a previous theorem.}}\\&&&{\text{Thus, }}{\bar {X}}\in L\iff {\mathfrak {M}}({\bar {X}}).\;\,\therefore {\mathfrak {M}}_{l}({\bar {X}})\iff {\mathfrak {M}}({\bar {X}}).\\\\&{\textbf {Theorem.}}&&{\mathfrak {Pr}}_{l}({\bar {X}})\iff {\mathfrak {Pr}}({\bar {X}}).\\&{\textbf {Proof.}}&&{\mathfrak {Pr}}_{l}({\bar {X}})\iff \neg {\mathfrak {M}}_{l}({\bar {X}})\iff \neg {\mathfrak {M}}({\bar {X}})\iff {\mathfrak {Pr}}({\bar {X}}).\\\\&{\textbf {Theorem.}}&&V_{l}=L.\\&{\textbf {Proof.}}&&\forall {\bar {u}}({\bar {u}}\in V_{l}).\\&&&\forall {\bar {u}}({\bar {u}}\in L).\;{\text{ Hence, }}\forall {\bar {u}}({\bar {u}}\in V_{l}\iff {\bar {u}}\in L).\\&&&{\text{Since }}L{\text{ is constructive, }}\;V_{l}=L{\text{ by constructive extensionality.}}\\\\&{\textbf {Theorem.}}&&\emptyset {\text{ is absolute}}.\\&{\textbf {Proof.}}&&\forall u(u\notin \emptyset )\implies \forall {\bar {u}}({\bar {u}}\notin \emptyset ).\;{\text{Also, }}\forall {\bar {u}}({\bar {u}}\notin \emptyset _{l}).\\&&&{\text{Since }}\emptyset {\text{ is constructive, }}\;\emptyset _{l}=\emptyset {\text{ by constructive extensionality.}}\\\\&{\textbf {Theorem.}}&&Un_{l}({\bar {F}})\iff Un({\bar {F}}).\\&{\textbf {Proof.}}&&Un_{l}({\bar {F}})\iff \forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}(({\bar {v}},{\bar {u}})\in {\bar {F}}\land ({\bar {w}},{\bar {u}})\in {\bar {F}}\implies {\bar {v}}={\bar {w}}).\\&&&Un({\bar {F}})\iff \forall u\,\forall v\,\forall w((v,u)\in {\bar {F}}\land (w,u)\in {\bar {F}}\implies v=w).\\&&&\qquad \quad \,\iff \forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}(({\bar {v}},{\bar {u}})\in {\bar {F}}\land ({\bar {w}},{\bar {u}})\in {\bar {F}}\implies {\bar {v}}={\bar {w}})\\&&&\qquad \qquad \qquad {\text{ by }}Abs_{3}{\text{ since }}(v,u)\in {\bar {F}}\land (w,u)\in {\bar {F}}\implies u,v,w\in L\\&&&\qquad \quad \,\iff Un_{l}({\bar {F}}).\\\\&{\textbf {Theorem.}}&&\cup _{l}{\bar {x}}=\cup {\bar {x}}.\\&{\textbf {Proof.}}&&\forall {\bar {u}}({\bar {u}}\in \cup _{l}{\bar {x}}\iff \exists {\bar {v}}({\bar {u}}\in {\bar {v}}\land {\bar {v}}\in {\bar {x}})).\\&&&{\text{Strategy: form the set }}\{(u,v)\in E\cap (L\times {\bar {x}})\}.{\text{ Then replace L with a set.}}\\&&&\cup {\bar {x}}\subseteq {\bar {w}}.\;\;{\text{Let }}{\bar {z}}=Dom(E\cap ({\bar {w}}\times {\bar {x}})).\\&&&u\in {\bar {z}}\iff u\in Dom(E\cap ({\bar {w}}\times {\bar {x}}))\\&&&\qquad \;\;\iff \exists v((u,v)\in E\land (u,v)\in {\bar {w}}\times {\bar {x}})\\&&&\qquad \;\;\iff \exists v(u\in v\land u\in {\bar {w}}\land v\in {\bar {x}})\\&&&\qquad \;\;\iff \exists v(u\in v\land v\in {\bar {x}})\;\;{\text{ (Since }}\exists v(u\in v\land v\in {\bar {x}})\implies u\in \cup {\bar {x}}\subseteq {\bar {w}}).\\&&&\qquad \;\;\iff u\in \cup {\bar {x}}\;\,{\text{ and }}\iff \exists {\bar {v}}({\bar {u}}\in {\bar {v}}\land {\bar {v}}\in {\bar {x}})\\&&&\qquad \qquad \qquad \qquad \qquad \quad \,\iff {\bar {u}}\in \cup _{l}{\bar {x}}.\\\end{alignedat}}$

L is a model of NBG

${\begin{alignedat}{2}&A1_{l}:&&{\mathfrak {L}}({\bar {x}}).\\&{\textbf {Proof.}}\;\;&&{\text{A previous theorem.}}\\\\&A2_{l}:&&{\bar {X}}\in {\bar {Y}}\implies {\mathfrak {M}}_{l}({\bar {X}}).\\&{\textbf {Proof.}}&&{\text{Using A2 and absoluteness of }}{\mathfrak {M}}:\;{\bar {X}}\in {\bar {Y}}\implies {\mathfrak {M}}({\bar {X}})\implies {\mathfrak {M}}_{l}({\bar {X}}).\\\\&A3_{l}:&&\forall {\bar {u}}({\bar {u}}\in {\bar {X}}\iff {\bar {u}}\in {\bar {Y}})\implies {\bar {X}}={\bar {Y}}.\\&{\textbf {Proof.}}&&{\text{By constructive extensionality.}}\\\\&A4_{l}:&&\forall {\bar {x}}\,\forall {\bar {y}}\,\exists {\bar {z}}\,\forall {\bar {u}}({\bar {u}}\in {\bar {z}}\iff {\bar {u}}={\bar {x}}\lor {\bar {u}}={\bar {y}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {z}}=\{{\bar {x}},{\bar {y}}\},{\text{ and use absoluteness of pairing operation.}}\\\\\end{alignedat}}$

${\begin{alignedat}{2}&B1_{l}:&&\exists {\bar {E}}\,\forall {\bar {u}}\,\forall {\bar {v}}(({\bar {u}},{\bar {v}})\in {\bar {E}}\iff {\bar {u}}\in {\bar {v}}).\\&{\textbf {Proof.}}\;\;&&{\text{Using B1, there exists an }}E:\forall u\forall v((u,v)\in E\iff u\in v).\\&&&{\text{Let }}{\bar {E}}=E\cap L.{\text{ By a previous theorem: }}{\mathfrak {L}}(E\cap L).\\&&&({\bar {u}},{\bar {v}})\in {\bar {E}}\implies ({\bar {u}},{\bar {v}})\in E\implies {\bar {u}}\in {\bar {v}}.\\&&&{\bar {u}}\in {\bar {v}}\implies ({\bar {u}},{\bar {v}})\in E.\;{\text{ Also, }}({\bar {u}},{\bar {v}})\in L.\\&&&{\text{Thus, }}\;{\bar {u}}\in {\bar {v}}\implies ({\bar {u}},{\bar {v}})\in E\cap L={\bar {E}}.\\&&&\therefore \;\,\forall {\bar {u}}\,\forall {\bar {v}}(({\bar {u}},{\bar {v}})\in {\bar {E}}\iff {\bar {u}}\in {\bar {v}}).\\\\&B2_{l}:&&\forall {\bar {A}}\,\forall {\bar {B}}\,\exists {\bar {C}}\,\forall {\bar {u}}({\bar {u}}\in {\bar {C}}\iff {\bar {u}}\in {\bar {A}}\land {\bar {u}}\in {\bar {B}}).\\&{\textbf {Proof.}}&&{\text{Using B2, let }}{\bar {C}}={\bar {A}}\cap {\bar {B}}.\;{\text{ By a previous theorem: }}{\mathfrak {L}}({\bar {A}}\cap {\bar {B}}).\\&&&{\text{B2 implies }}\,\forall u(u\in {\bar {C}}\iff u\in {\bar {A}}\land u\in {\bar {B}}).\\&&&\therefore \;\forall {\bar {u}}({\bar {u}}\in {\bar {C}}\iff {\bar {u}}\in {\bar {A}}\land {\bar {u}}\in {\bar {B}}).\\&&&{\text{We can also prove that }}\cap _{l}{\text{ is absolute, but this is not needed here.}}\\\\&B3_{l}:&&\forall {\bar {A}}\,\exists {\bar {B}}\,\forall {\bar {u}}({\bar {u}}\in {\bar {B}}\iff {\bar {u}}\notin {\bar {A}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {B}}=L\setminus {\bar {A}}.\;{\text{ By a previous theorem: }}{\mathfrak {L}}(L\setminus {\bar {A}}).\\&&&\forall u(u\in {\bar {B}}\iff u\in L\land u\notin {\bar {A}}).\\&&&\therefore \;{\bar {u}}({\bar {u}}\in {\bar {B}}\iff {\bar {u}}\in L\land {\bar {u}}\notin {\bar {A}}\iff {\bar {u}}\notin {\bar {A}}).\\\\&B4_{l}:&&\forall {\bar {A}}\,\exists {\bar {B}}\,\forall {\bar {u}}({\bar {u}}\in {\bar {B}}\iff \exists {\bar {v}}(({\bar {v}},{\bar {u}})\in {\bar {A}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {B}}=Dom({\bar {A}}).\;{\text{ By a previous theorem: }}{\mathfrak {L}}(Dom({\bar {A}})).\\&&&\forall u{\bigl [}u\in {\bar {B}}\iff \exists v((v,u)\in {\bar {A}}){\bigr ]}.\\&&&\therefore \;\forall {\bar {u}}{\bigl [}{\bar {u}}\in {\bar {B}}\iff \exists v((v,{\bar {u}})\in {\bar {A}})\iff \exists {\bar {v}}(({\bar {v}},{\bar {u}})\in {\bar {A}}){\bigr ]}.\\\\&B5_{l}:&&\forall {\bar {A}}\,\exists {\bar {B}}\,\forall {\bar {u}}\,\forall {\bar {v}}(({\bar {v}},{\bar {u}})\in {\bar {B}}\iff {\bar {u}}\in {\bar {A}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {B}}=L\times {\bar {A}}.\;{\text{ By a previous theorem: }}{\mathfrak {L}}(L\times {\bar {A}}).\\&&&\forall u\,\forall v{\bigl [}(v,u)\in {\bar {B}}\iff ({\bar {v}}\in L\land {\bar {u}}\in {\bar {A}})\,{\bigr ]}.\\&&&\therefore \;\forall {\bar {u}}\,\forall {\bar {v}}{\bigl [}({\bar {v}},{\bar {u}})\in {\bar {B}}\iff ({\bar {v}}\in L\land {\bar {u}}\in {\bar {A}})\iff {\bar {u}}\in {\bar {A}}\,{\bigr ]}.\\\\&B6_{l}:&&\forall {\bar {A}}\,\exists {\bar {B}}\,\forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}(({\bar {u}},{\bar {v}},{\bar {w}})\in {\bar {B}}\iff ({\bar {v}},{\bar {u}},{\bar {w}})\in {\bar {A}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {B}}=Tr({\bar {A}}).\;{\text{ By a previous theorem: }}{\mathfrak {L}}(Tr({\bar {A}})).\\&&&\forall u\,\forall u\,\forall w{\bigl [}(u,v,w)\in {\bar {B}}\iff (v,u,w)\in {\bar {A}}{\bigr ]}.\\&&&\therefore \;\forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}{\bigl [}({\bar {u}},{\bar {v}},{\bar {w}})\in {\bar {B}}\iff ({\bar {v}},{\bar {u}},{\bar {w}})\in {\bar {A}}{\bigr ]}.\\\\&B7_{l}:&&\forall {\bar {A}}\,\exists {\bar {B}}\,\forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}(({\bar {w}},{\bar {u}},{\bar {v}})\in {\bar {B}}\iff ({\bar {u}},{\bar {v}},{\bar {w}})\in {\bar {A}}).\\&{\textbf {Proof.}}&&{\text{Let }}{\bar {B}}=Cp({\bar {A}}).\;{\text{ By a previous theorem: }}{\mathfrak {L}}(Cp({\bar {A}})).\\&&&\forall u\,\forall u\,\forall w{\bigl [}(w,u,v)\in {\bar {B}}\iff (u,v,w)\in {\bar {A}}{\bigr ]}.\\&&&\therefore \;\forall {\bar {u}}\,\forall {\bar {v}}\,\forall {\bar {w}}{\bigl [}({\bar {w}},{\bar {u}},{\bar {v}})\in {\bar {B}}\iff ({\bar {u}},{\bar {v}},{\bar {w}})\in {\bar {A}}{\bigr ]}.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&C1_{l}:&&\exists {\bar {a}}{\bigl [}\neg {\mathfrak {Em}}({\bar {a}})\land \forall {\bar {x}}({\bar {x}}\in {\bar {a}}\implies \exists {\bar {y}}({\bar {y}}\in {\bar {a}}\land {\bar {x}}\subset {\bar {y}})){\bigr ]}.\\&{\textbf {Proof.}}\;\;&&{\text{Let }}{\bar {a}}=F(J(0,\omega ,0)).\\&&&(i,\alpha ,\beta )\;S\;(0,\omega ,0)\implies (\alpha ,\beta )\;R\;(\omega ,0)\lor ((\alpha ,\beta )=(\omega ,0)\land i<0{\text{ [latter disjunct cannot occur.]}}\\&&&(\alpha ,\beta )\;R\;(\omega ,0)\iff Max(\alpha ,\beta )<Max(\omega ,0)\lor (Max(\alpha ,\beta )=Max(\omega ,0)\land (\alpha ,\beta )\;Le\;(\omega ,0).)\\&&&(\alpha ,\beta )\;Le\;(\omega ,0)\iff \beta <0\lor (\beta =0\land \alpha <\omega ).\\&&&{\text{Last two cases imply: }}\alpha ,\beta <\omega .\\&&&\therefore \;{\bar {x}}\in {\bar {a}}\implies {\bar {x}}=F(J(i,\alpha ,\beta ))<F(J(0,\omega ,0))\implies \alpha ,\beta <\omega \implies J(i,\alpha ,\beta )=n<\omega .\\&&&\emptyset \in {\bar {a}}\implies \neg {\mathfrak {Em}}({\bar {a}}).\\&&&{\text{We now prove }}{\bar {x}}\in {\bar {a}}\implies {\bar {x}}\cup \{{\bar {x}}\}\in {\bar {a}}:\;\,{\bar {x}}\in {\bar {a}}\implies \exists n<\omega ({\bar {x}}=F(n)).\\&&&{\text{Then }}\{{\bar {x}}\}=\{{\bar {x}},{\bar {x}}\}=F(J((p,n,n))=F(J(n_{1})).\;\;{\bar {x}}\cup \{{\bar {x}}\}\subseteq {\bar {z}}=F(J((0,n_{1}+1,0))).\\&&&{\text{Then }}{\bar {x}}\cup \{{\bar {x}}\}={\bar {z}}\setminus (z\setminus {\bar {x}})\setminus \{{\bar {x}}\})=F(n_{2})\in F(J((0,\omega ,0))).\\&&&{\text{Let }}{\bar {y}}={\bar {x}}\cup \{{\bar {x}}\}.\;\;\therefore \;{\bar {y}}\in {\bar {a}}\land {\bar {x}}\subset {\bar {y}}.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&{\textbf {Definition.}}\;\;(\alpha ,\beta )\;Le\;(\gamma ,\delta )\iff \beta <\delta \lor (\beta =\delta \land \alpha <\gamma ).\\&{\textbf {Definition.}}\;\;(\alpha ,\beta )\;R\;(\gamma ,\delta )\iff Max(\alpha ,\beta )<Max(\gamma ,\delta )\lor (Max(\alpha ,\beta )=Max(\gamma ,\delta )\land (\alpha ,\beta )\;Le\;(\gamma ,\delta ))\\&{\textbf {Definition.}}\;\;(i,\alpha ,\beta )\;S\;(j,\gamma ,\delta )\iff (\alpha ,\beta )\;R\;(\gamma ,\delta )\lor ((\alpha ,\beta )=(\gamma ,\delta )\land i<j.\\\\\end{alignedat}}$

${\begin{alignedat}{2}&C2_{l}:&&\forall {\bar {x}}\,\exists {\bar {y}}\,\forall {\bar {u}}\,\forall {\bar {v}}{\bigl [}({\bar {u}}\in {\bar {v}}\land {\bar {v}}\in {\bar {x}})\implies {\bar {u}}\in {\bar {y}}{\bigr ]}.\\&{\textbf {Proof.}}\;\;&&{\text{Using axiom C2: }}{\text{ Let }}y{\text{ satisfy }}\forall u\,\forall v(u\in v\land v\in {\bar {x}}\implies u\in y).\\&&&{\text{Since }}L\cap y\subseteq L,{\text{ there is a }}{\bar {z}}{\text{ such that }}L\cap y\subseteq {\bar {z}}.\\&&&{\bar {z}}{\text{ satisfies }}C2_{l}:({\bar {u}}\in {\bar {v}}\land {\bar {v}}\in {\bar {x}})\implies {\bar {u}}\in y\implies {\bar {u}}\in L\cap y\implies {\bar {u}}\in {\bar {z}}.\\\\&C3_{l}:&&\forall {\bar {x}}\,\exists {\bar {y}}\,\forall {\bar {u}}{\bigl [}({\bar {u}}\subseteq {\bar {x}}\implies {\bar {u}}\in {\bar {y}}{\bigr ]}.\\&{\textbf {Proof.}}&&{\text{Using axiom C3: }}{\text{ Let }}y{\text{ satisfy }}\forall u(u\subseteq {\bar {x}}\implies u\in y).\\&&&{\text{Since }}L\cap y\subseteq L,{\text{ there is a }}{\bar {z}}{\text{ such that }}L\cap y\subseteq {\bar {z}}.\\&&&{\bar {z}}{\text{ satisfies }}C3_{l}:{\bar {u}}\subseteq {\bar {x}}\implies {\bar {u}}\in y\implies {\bar {u}}\in L\cap y\implies {\bar {u}}\in {\bar {z}}.\\\\&C4_{l}:&&\forall {\bar {x}}\,\forall {\bar {F}}{\bigl [}Un({\bar {F}})\implies \exists {\bar {y}}\,\forall {\bar {v}}({\bar {v}}\in {\bar {y}}\iff \exists {\bar {u}}({\bar {u}}\in {\bar {x}})\land ({\bar {v}},{\bar {u}})\in {\bar {F}}){\bigr ]}.\\&{\textbf {Proof.}}&&{\text{Using axiom C4: Given }}{\bar {x}}{\text{ and }}{\bar {F}},{\text{ there is a }}y{\text{ such that }}\forall v(v\in y\iff \exists u(u\in {\bar {x}}\land (v,u)\in {\bar {F}})).\\&&&{\text{Now }}y={\bar {F}}[{\bar {x}}]\implies {\mathfrak {M}}({\bar {F}}[{\bar {x}}]).\;{\text{By a previous theorem, }}{\mathfrak {L}}({\bar {F}}[{\bar {x}}]).\;\,\therefore y\in L.\\&&&{\text{Since }}(v\in y\implies v\in L)\land (u\in {\bar {x}}\implies u\in L),{\text{ we have: }}\,\exists {\bar {y}}\,\forall {\bar {v}}({\bar {v}}\in {\bar {y}}\iff \exists {\bar {u}}({\bar {u}}\in {\bar {x}})\land ({\bar {v}},{\bar {u}})\in {\bar {F}}).\\\\&&&{\text{*********** CHECK NEXT 2: HAVE WE STATED D1 and E1 correctly?? }}\\\\&D1_{l}:&&\neg {\mathfrak {Em}}({\bar {A}})\implies \exists {\bar {u}}{\bigl [}{\bar {u}}\in {\bar {A}}\land {\mathfrak {Ex}}({\bar {u}},{\bar {A}}){\bigr ]}.\\&{\textbf {Proof.}}&&{\text{Let }}\neg {\mathfrak {Em}}({\bar {A}}).\;{\text{Using axiom D1: }}{\text{ Let }}u{\text{ satisfy }}u\in {\bar {A}}\land {\mathfrak {Ex}}(u,{\bar {A}})).\\&&&{\text{Since }}u\in {\bar {A}}\implies u\in L,{\text{ we have: }}\,\exists {\bar {u}}{\bigl [}{\bar {u}}\in {\bar {A}}\land {\mathfrak {Ex}}({\bar {u}},{\bar {A}}{\bigr ]}.\\\\&E1_{l}:&&\exists {\bar {G}}\,\forall {\bar {x}}{\bigl [}{\mathfrak {Un}}({\bar {G}})\land \exists {\bar {y}}(\neg {\mathfrak {Em}}({\bar {x}})\implies ({\bar {y}},{\bar {x}})\in {\bar {G}}){\bigr ]}.\\&{\textbf {Proof.}}&&{\text{Define: }}({\bar {y}},{\bar {x}})\in {\bar {G}}\iff {\bar {y}}\in {\bar {x}}\land \forall {\bar {z}}(Od({\bar {y}})\leq Od({\bar {z}})).\\&&&{\text{Must prove: }}{\mathfrak {L}}({\bar {G}}).{\text{Follows from Class Existence Theorem, but must prove that Od is absolute.}}\\\end{alignedat}}$