Theorem. O r d ( X ) & u ∈ X ⟹ S e g E ( X , u ) = u . Proof. P r e d E ( u ) = u by definition of E . u ⊆ X since T r a n s ( X ) . ∴ S e g E ( X , u ) = X ∩ P r e d E ( u ) = X ∩ u = u . {\displaystyle {\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}}}
Theorem. O r d ( Y ) & X ⊂ Y & T r a n s ( X ) ⟹ X ∈ Y . Proof. Let u = l e a s t ( Y ∖ X ) . x ∈ u ⟹ x ∈ X : Since u = l e a s t ( Y ∖ X ) , x ∈ X . x ∈ X ⟹ x ∈ u : Let x ∈ X . If x = u , then x ∉ X . Contradiction. If u ∈ x , then T r a n s ( X ) ⟹ u ∈ X . Contradiction. ∴ x ∈ u . By extensionality, X = u . ∴ X ∈ Y . {\displaystyle {\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}}}
Theorem. O r d ( X ) & O r d ( Y ) ⟹ Only one of the following holds: X ∈ Y , X = Y , Y ∈ X . Proof. T r a n s ( X ) & T r a n s ( Y ) ⟹ T r a n s ( X ∩ Y ) . Assume X ⊈ Y & Y ⊈ X . Then X ∩ Y ≠ X & X ∩ Y ≠ Y . Hence, X ∩ Y ⊂ X & X ∩ Y ⊂ Y . By the previous theorem, O r d ( X ) & T r a n s ( X ∩ Y ) & X ∩ Y ⊂ X ⟹ X ∩ Y ∈ X . Similarly, X ∩ Y ∈ Y . Thus, X ∩ Y ∈ X ∩ Y , which contradicts regularity . ∴ X ⊆ Y ∨ Y ⊆ X , which implies X ⊂ Y ∨ X = Y ∨ Y ⊂ X . There are 3 ways for 2 of these 3 to be true: ( X ⊂ Y & X = Y ) ∨ ( X = Y & Y ⊂ X ) ∨ ( X ⊂ Y & Y ⊂ X ) . Each of these implies X ⊂ X , which is a contradiction. Therefore, only one of the three holds. By the previous theorem, this implies that only one of the following holds: X ∈ Y , X = Y , Y ∈ X . {\displaystyle {\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}}}
Theorem. E C o n n e x O n . Proof. Implied by the previous theorem. {\displaystyle {\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;E\,Connex\,On.\\&{\textbf {Proof.}}\;\;{\text{Implied by the previous theorem.}}\\\\\end{alignedat}}}
Theorem. O r d ( A ) & X ∈ A ⟹ O r d ( X ) . Proof. O r d ( A ) ⟹ X ⊆ A . ∴ E W e l l A ⟹ E W e l l X . Let Z ∈ Y ∈ X ∈ A . T r a n s ( A ) ⟹ Z , Y , X ∈ A . E W e l l A & Z ∈ Y ∈ X ⟹ Z ∈ X . ∴ T r a n s ( X ) . ∴ E W e l l X & T r a n s ( X ) ⟹ O r d ( X ) . {\displaystyle {\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}}}
Theorem. O r d ( A ) ⟹ A ⊆ O n . Proof. Let X ∈ A . Since O r d ( A ) , the previous theorem implies O r d ( X ) . Since X is a set, X ∈ O n . ∴ A ⊆ O n . {\displaystyle {\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}}}
Theorem. T r a n s ( O n ) . Proof. Since A ∈ O n implies O r d ( A ) , the previous theorem implies A ⊆ O n . ∴ T r a n s ( O n ) . {\displaystyle {\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}}}
Theorem. O r d ( O n ) . Proof. Follows from earlier theorems that imply E C o n n e x O n & T r a n s ( O n ) . {\displaystyle {\begin{alignedat}{2}&{\textbf {Theorem.}}\;\;Ord(On).\\&{\textbf {Proof.}}\;\;{\text{Follows from earlier theorems that imply }}E\,Connex\,On\;\And \;Trans(On).\\\\\end{alignedat}}}
Theorem. ∀ X ( X ⊆ O n ⟹ E W e l l X ) . Proof. O r d ( O n ) ⟹ E W e l l O n ⟹ E W e l l X for all X ⊆ O n . {\displaystyle {\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}}}
Theorem. ∀ x ( x ∈ A ⟹ T r a n s ( x ) ) ⟹ T r a n s ( ∪ A ) . Proof. Let u ∈ v ∈ ∪ A . There exists a w such that v ∈ w ∈ A . T r a n s ( w ) & u ∈ v ∈ w ⟹ u ∈ w . Since u ∈ w ∈ A ⟹ u ∈ ∪ A , we have T r a n s ( ∪ A ) . {\displaystyle {\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}}}
Theorem. A ⊆ T & T r a n s ( T ) ⟹ ∪ A ⊆ T . Proof. Let u ∈ ∪ A . Then there exists a v such that u ∈ v ∈ A . A ⊆ T ⟹ u ∈ v ∈ T . T r a n s ( T ) ⟹ u ∈ T . ∴ ∪ A ⊆ T . {\displaystyle {\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}}}
Theorem. A ⊆ O n ⟹ O r d ( ∪ A ) . Proof. Use last two theorems. First implies T r a n s ( ∪ A ) since ∀ x [ x ∈ A ⊆ O n ⟹ T r a n s ( x ) ] . Second implies E W e l l ∪ A since A ⊆ O n & T r a n s ( O n ) ⟹ ∪ A ⊆ O n . ∴ O r d ( ∪ A ) . {\displaystyle {\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}}}
Theorem. α + 1 = α ∪ { α } is the ordinal that follows α . Proof. T r a n s ( α + 1 ) : β ∈ α ∪ { α } ⟹ β ∈ α ∨ β = α . Now β ∈ α ⟹ β ⊆ α and β = α ⟹ β ⊆ { α } . ∴ β ⊆ α ∪ { α } . E W e l l α + 1 since we have just added one set to the end of the well-ordered set α . ∴ O r d ( α + 1 ) . Next we prove: α < β ⟹ α + 1 ≤ β . α ∈ β ⟹ α ⊆ β . Also, α ∈ β ⟹ { α } ⊆ β ∴ α ∪ { α } ⊆ β . This implies α ∪ { α } ∈ β ∨ α ∪ { α } = β . ∴ α ∪ { α } ≤ β . Gödel proves β ∈ α + 1 ⟹ β ≤ α : β ∈ α ∪ { α } ⟹ β ∈ α ∨ β = α ⟹ β ≤ α . {\displaystyle {\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}}}
Theorem. If β > α ⟹ F ( β ) > F ( α ) , then ∀ α ( F ( α ) ≥ α ) . Proof. By contradiction. Assume ∃ α ( F ( α ) < α ) and let α = l e a s t { α : F ( α ) < α } . Then F ( α ) = β < α . However, F ( β ) ≥ β & F ( α ) > F ( β ) ⟹ F ( α ) > β . Contradiction. {\displaystyle {\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}}}
Theorem. O r d ( X ) & O r d ( Y ) & F I s o m E , E ( X , Y ) ⟹ X = Y & F = I ↾ X . Proof. Let α = l e a s t { α ∈ X : F ( α ) ≠ α } and let F ( α ) = β . β < α : Then F ( α ) = β = F ( β ) , contradicting F being one-to-one . β > α : If γ < α , then F ( γ ) = γ < α . If γ ≥ α , then F ( γ ) ≥ F ( α ) = β > α , contradicting F being onto. Thus, ∀ α ∈ X ( F ( α ) = α ) . Since F is an isomorphism, Y = R n g ( F ) = X & F = I ↾ X . {\displaystyle {\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}}}
Theorem. ∀ G ∃ ! F [ F F n O n & ∀ α ( F ( α ) = G ( F ↾ α ) ] . Proof. Strategy: Define class K consisting of all functions f that approximate F on β . Let: f ∈ K ⟺ ∃ β [ f F n β & ∀ α ( α ∈ β ⟹ f ( α ) = G ( f ↾ α ) ) ] f 1 F n β 1 ∈ K & f 2 F n β 2 ∈ K & β 1 < β 2 ⟹ f 1 ⊆ f 2 : Assume conclusion is false. Let α = l e a s t { γ : f 1 ( γ ) ≠ f 2 ( γ ) } . However, f 1 ( α ) = G ( f 1 ↾ α ) ) = G ( f 2 ↾ α ) ) = f 2 ( α ) , contradicting our assumption. ∴ f 1 ⊆ f 2 . ∀ α ( ∃ ! f ( f ∈ K & f F n α & ∀ β < α ( F ( β ) = G ( F ↾ β ) ] ) : Assume false and let α be least such that it is false. However, since α is least, we can define a function f by: h = ∪ { g ∈ K : β < α ∧ g F n β } ; f = h ∪ { ⟨ α , G ( h ↾ α ) ⟩ } , contradicting our assumption. Let F = ∪ K . F F n O n & ∀ α ( F ( α ) = G ( F ↾ α ) ) : The first statement proved above implies that F is a function satisfying the recursive definition. The second statement implies that D o m ( F ) = O n . {\displaystyle {\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}}}
Theorem. P r ( A ) & W W e l l A & All proper initial segments of A are sets ⟹ I s o m E , W ( O n , A ) . Proof. Define: F ( α ) = l e a s t ( A ∖ F ↾ α ) . If ∀ β ( β < α ⟹ S e g W ( A , F ( β ) ) = F ↾ β is a proper initial segment of A ) , then S e g W ( A , F ( α ) ) = F ↾ α is a proper initial segment of A . Proof by transfinite induction: α = 0 : S e g W ( A , F ( 0 ) ) = ∅ = F ↾ ∅ , which is a proper initial segment. α = β + 1 : S e g W ( A , F ( α ) ) = S e g W ( A , F ( β ) ) ∪ { F ( β ) } = F ↾ β ∪ { F ( β ) } = F ↾ α , which is a proper initial segment since F ( β ) is ordinal following ordinals in S e g W ( A , F ( β ) ) . α = L i m { β : β < α } : S e g W ( A , F ( α ) ) = ∪ { S e g W ( A , F ( β ) ) : β < α } = ∪ { F ↾ β : β < α } = F ↾ α , which is a proper initial segment since F ( α ) is ordinal following ordinals in ∪ { S e g W ( A , F ( β ) ) : β < α } . F preserves ordering : β < α ⟹ F ( β ) W F ( α ) : F ( β ) ∈ F ↾ α = S e g W ( A , F ( α ) ) ⟹ F ( β ) W F ( α ) . D o m ( F ) = O n : Let α ∈ O n . By replacement F ↾ α is a set. Since A is a proper class, A ∖ F ↾ α is a proper class, so it is non-empty. Thus, F ( α ) = l e a s t ( A ∖ F ↾ α ) is defined. ∴ D o m ( F ) = O r d . R n g ( F ) = A : Assume R n g ( F ) ⊂ A . Let y = l e a s t { x ∈ A : x ∉ R n g ( F ) } and let X = { x : x W y } . Since X is a proper initial segment, it is a set. F is a bijection from O n to X , so F − 1 is a bijection from X to O r d . By replacement, F − 1 [ X ] = O n is a set, contradicting O n being a proper class. ∴ R n g ( F ) = A . {\displaystyle {\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}}}
Theorem. If a is a set and W W e l l a , then ∃ α ( α ∈ O n ∧ I s o m E , W ( α , a ) ) . Proof. Define: f ( β ) = l e a s t ( a ∖ f ↾ β ) . Same proof of properties as in last theorem with the difference that the construction terminates at α . Assume it does not terminate at any ordinal number α . Then f is a bijection from O n to a subset of a . So f − 1 is a bijection from a subset of a to O n . By replacement, f − 1 [ a ] = O n is a set, contradicting O n being a proper class. ∴ ∃ α ( α ∈ O n ∧ I s o m E , W ( α , a ) ) . {\displaystyle {\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}}}
Definition. ( α , β ) L e ( γ , δ ) ⟺ β < δ ∨ ( β = δ ∧ α < γ ) . Definition. ( α , β ) R ( γ , δ ) ⟺ M a x ( α , β ) < M a x ( γ , δ ) ∨ ( M a x ( α , β ) = M a x ( γ , δ ) ∧ ( α , β ) L e ( γ , δ ) ) Theorem. R well-orders O n 2 . Proof. R C o n n e x O n 2 : Follows from M a x ( α , β ) < M a x ( γ , δ ) , M a x ( α , β ) = M a x ( γ , δ ) , or M a x ( α , β ) > M a x ( γ , δ ) ; and similar inequalities holding between β and δ , and α and γ . R W e l l O n 2 : Let U ⊆ O n 2 . Let m i n 1 = l e a s t { M a x ( α , β ) : ( α , β ) ∈ U } and let U 1 = { ( α , β ) ∈ U : M a x ( α , β ) = m i n 1 } . Then ∀ ( α , β ) ∈ U 1 ( M a x ( α , β ) = m i n 1 ) and ∀ ( α , β ) ∈ U ∖ U 1 [ M a x ( α , β ) > m i n 1 ) . Let m i n 2 = l e a s t { β : ( α , β ) ∈ U 1 } and let U 2 = { ( α , β ) ∈ U 1 : β = m i n 2 } . Then ∀ ( α , β ) ∈ U 2 ( β = m i n 2 ) and ∀ ( α , β ) ∈ U 1 ∖ U 2 ( β > m i n 2 ) . Let m i n 3 = l e a s t { α : ( α , β ) ∈ U 2 } and let U 3 = { ( α , β ) ∈ U 2 : α = m i n 3 } . Then ∀ ( α , β ) ∈ U 3 ( α = m i n 3 ) and ∀ ( α , β ) ∈ U 2 ∖ U 3 ( α > m i n 3 ) . Now m i n = ( m i n 3 , m i n 2 ) is the only member of U 3 . Since m i n ∈ U 3 ⊆ U 2 ⊆ U 1 ⊆ U , the above properties imply m i n < ( α , β ) for all ( α , β ) ∈ U ∖ U 3. {\displaystyle {\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}}}
Theorem. P r ( O n 2 ) & All proper initial segments of ( O n 2 , R ) are sets. Therefore, I s o m E , R ( O n , O n 2 ) . Proof. P r ( O n ) ⟹ P r ( O n 2 ) . Let S = S e g R ( O n 2 , ( α , β ) ) be a proper initial segment and let δ = M a x ( α , β ) . S ⊆ S e g R ( O n 2 , ( δ , δ ) + 1 ) ⊆ ( δ + 1 ) × ( δ + 1 ) , which is a set. ∴ S is a set. {\displaystyle {\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}}}
Theorem. If F I s o m E , < ( O n , O n 2 ) as defined above and P = F − 1 , then P ( ( α , β ) ) ≥ m a x ( α , β ) . Proof. This follows from: F ( m a x ( α , β ) ) ≤ ( m a x ( α , β ) , 0 ) ≤ ( α , β ) since applying P gives: m a x ( α , β ) ≤ P ( ( m a x ( α , β ) , 0 ) ) ≤ P ( ( α , β ) ) . All we need to prove is: F ( α ) ≤ ( α , 0 ) . α = β + 1 : F ( β + 1 ) = F ( β ) + 1 ≤ ( α , 0 ) + 1 ≤ ( α + 1 , 0 ) . α = L i m { β : β < α } : Lemma: If F is an isomorphism and a = L i m { b : b < a } , then F ( a ) = L i m { F ( b ) : b < a } . Proof: If F is an isomorphism and a = L i m { b : b < a } , then a can be defined as a ≠ l e a s t ( A ) ∧ ¬ ∃ b ( a = b + 1 ) ∧ a = l e a s t ( A ∖ { b : b < a } ) . Since F is an isomorphism, F ( a ) ≠ l e a s t ( F ( A ) ) ∧ ¬ ∃ F ( b ) ( F ( a ) = F ( b ) + 1 ) ∧ F ( a ) = l e a s t ( F ( A ) ∖ { F ( b ) : F ( b ) < F ( a ) } ) . ∴ F ( a ) = L i m { F ( b ) : F ( b ) < F ( a ) } = L i m { F ( b ) : b < a } . ∴ F ( α ) = L i m { F ( β ) : β < α } ≤ L i m { ( β , 0 ) : β < α } = ( α , 0 ) . The last equality holds since L i m { ( β , 0 ) : β < α } = l e a s t ( O n 2 ∖ ∪ { s e g R ( O n 2 , ( β , 0 ) ) : ( β , 0 ) R ( α , 0 ) } ) = ( α , 0 ) . Gödel's proof is much shorter: P ( ( α , β ) ) ≥ P ( ( m a x ( α , β ) , 0 ) ) . Let γ = m a x ( α , β ) . Because P ( ( γ , 0 ) ) is strictly increasing, P ( ( γ , 0 ) ) ≥ γ . ∴ P ( ( α , β ) ) ≥ P ( ( m a x ( α , β ) , 0 ) ) ≥ m a x ( α , β ) . {\displaystyle {\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}}}
Definition. ( i , α , β ) S ( j , γ , δ ) ⟺ ( α , β ) R ( γ , δ ) ∨ ( ( α , β ) = ( γ , δ ) ∧ i < j . Theorem. P r ( 8 × O n 2 ) & All proper initial segments of ( 8 × O n 2 , S ) are sets. Therefore, I s o m E , S ( O n , 8 × O n 2 ) . Proof. P r ( O n ) ⟹ P r ( 8 × O n 2 ) . Let A = S e g S ( 8 × O n 2 , ( i , α , β ) ) be a proper initial segment and let δ = M a x ( α , β ) . A ⊆ S e g S ( 8 × O n 2 , ( 8 , δ , δ ) + 1 ) ⊆ 8 × ( δ + 1 ) × ( δ + 1 ) , which is a set. ∴ A is a set. {\displaystyle {\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}}}
Definition. J F n ( 8 × O n 2 ) ∧ R n g ( J ) = O n ∧ i , j < 8 ⟹ [ ( i , α , β ) S ( j , γ , δ ) ⟹ J ( ( i , α , β ) ) < J ( ( j , γ , δ ) ) ] . Definition. For 0 ≤ i ≤ 7 : J i ( ( α , β ) ) = J ( ( i , α , β ) ) . Theorem. The R n g ( J i ) are mutually exclusive and their union is O n . Proof. The ranges are mutually exclusive because J is one-to-one. The union of the ranges is O n because J is onto O n . {\displaystyle {\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}}}
For any γ , there is a unique ( i , α , β ) such that γ = J ( i , α , β ) . {\displaystyle {\text{For any }}\gamma ,{\text{ there is a unique }}(i,\alpha ,\beta ){\text{ such that }}\gamma =J(i,\alpha ,\beta ).} ∴ There are functions K 1 and K 2 on O n such that K 1 ( J i ( α , β ) ) = α & K 2 ( J i ( α , β ) ) = β . {\displaystyle \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 .}
Definition. ( α , γ ) ∈ K 1 ⟺ ∃ i < 8 ∃ β ( γ = J ( ( i , α , β ) ) ) ∧ K 1 ⊆ O n 2 . Definition. ( β , γ ) ∈ K 2 ⟺ ∃ i < 8 ∃ α ( γ = J ( ( i , α , β ) ) ) ∧ K 2 ⊆ O n 2 . Theorem. J i ( ( α , β ) ) ≥ m a x ( α , β ) , J i ( ( α , β ) ) > m a x ( α , β ) for i > 0 , K 1 ( α ) ≤ α , K 1 ( α ) < α for α ∉ R n g ( J 0 ) , K 2 ( α ) ≤ α , K 2 ( α ) < α for α ∉ R n g ( J 0 ) . Proof. J ( ( i , α , β ) ) ≥ J ( ( i , ( m a x ( α , β ) , 0 ) ) . Because J ( ( i , ( m a x ( α , β ) , 0 ) ) is strictly increasing, J ( ( i , γ , 0 ) ) ≥ γ . ∴ For i > 0 : J ( ( i , α , β ) ) > J ( ( 0 , α , β ) ) ≥ J ( ( 0 , ( m a x ( α , β ) , 0 ) ) ≥ m a x ( α , β ) . Since for i > 0 : J ( ( i , α , β ) ) > J ( ( 0 , α , β ) ) ≥ α . We have i > 0 : K 1 ( J ( ( i , α , β ) ) ) > K 1 ( J ( ( 0 , α , β ) ) ) ≥ K 1 ( α ) . For all α : K 1 ( α ) ≤ K 1 ( J ( ( i , α , β ) ) ) = α . For all α ∉ R n g ( J 0 ) : i > 0 ∧ K 1 ( α ) ≤ K 1 ( J ( ( 0 , α , β ) ) ) < K 1 ( J ( ( i , α , β ) ) ) = α . Similarly for K 2 ( α ) . {\displaystyle {\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}}}
Definition. The following definitions are for subscripts i in J i , F i ( X , Y ) , q i and Q i . p = 1 // Pair e = 2 // Epsilon m = 3 // Minus for set minus (set difference) v = 4 // Product by V d = 5 // Domain t = 6 // Transposition c = 7 // Circular permutation {\displaystyle {\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}}}
Define the element functions: q 5 = q d = d o m where d o m ( ( y , x ) ) = x ∧ d o m F n V 2 . q 6 = q t = t r a n s where t r ( ( x , y , z ) ) = ( y , x , z ) ∧ t r F n V 3 . q 7 = q c = c p where c p ( ( x , y , z ) ) = ( z , x , y ) ∧ c p F n V 3 . t r 2 ( ( x , y ) = ( y , x ) ∧ t r 2 F n V 2 . {\displaystyle {\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}}}
Define the class functions: Q 5 = Q d = D o m where D o m ( X ) = d o m [ X ] . Q 6 = Q t = T r where T r ( X ) = t r [ X ] . Q 7 = Q c = C p where C p ( X ) = c p [ X ] . Q 4 = Q v = P v where P v ( X ) = d o m − 1 [ X ] = V × X . NOTE: d o m − 1 refers to inverse of the relation d o m . T r 2 ( X ) = t r 2 [ X ] . {\displaystyle {\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}}}
Define the set construction operators: F 1 ( X , Y ) = F p ( X , Y ) = { X , Y } , F 2 ( X , Y ) = F e ( X , Y ) = E ∩ X , F 3 ( X , Y ) = F m ( X , Y ) = X ∖ Y , F 4 ( X , Y ) = F v ( X , Y ) = X ∩ P v ( Y ) , // Product by V F 5 ( X , Y ) = F d ( X , Y ) = X ∩ D o m ( Y ) , // Domain F 6 ( X , Y ) = F t ( X , Y ) = X ∩ T r ( Y ) , // Transposition F 7 ( X , Y ) = F c ( X , Y ) = X ∩ C p ( Y ) , // Circular permutation {\displaystyle {\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}}}
In the following, 1 ≤ i ≤ 7. {\displaystyle {\text{In the following, }}1\leq i\leq 7.}
Definition. α ∈ R n g ( J 0 ) ⟹ F ( α ) = R n g ( F ↾ α ) , α ∈ R n g ( J i ) ⟹ F ( α ) = F i ( F ( K 1 ( α ) ) , F ( K 2 ( α ) ) ) , F F n O n . Theorem. The function F exists. Proof. By transfinite recursion. Define the function G ⊆ V 2 : ( x , y ) ∈ G ⟺ D o m ( x ) ∈ R n g ( J 0 ) ⟹ y = R n g ( x ) , ⟺ D o m ( x ) ∈ R n g ( J i ) ⟹ y = F i ( x ( K 1 ( D o m ( x ) ) , x ( K 2 ( D o m ( x ) ) ) , ⟺ otherwise, y = ∅ . So by transfinite recursion, the function F = G ( F ↾ α ) exists. We now prove this function is the function in the above definition. We have D o m ( x ) = D o m ( F ↾ α ) = α . Since i > 0 , for α ∈ R n g ( J i ) , K 1 ( D o m ( x ) ) = K 1 ( α ) < α and K 2 ( D o m ( x ) ) = K 2 ( α ) < α . This implies x ( K 1 ( D o m ( x ) ) = F ↾ α ( K 1 ( α ) ) = F ( K 1 ( α ) ) and similarly for x ( K 2 ( D o m ( x ) ) . ∴ α ∈ R n g ( J 0 ) ⟹ F ( α ) = R n g ( F ↾ α ) , α ∈ R n g ( J i ) ⟹ F ( α ) = F i ( F ( K 1 ( α ) ) , F ( K 2 ( α ) ) ) . {\displaystyle {\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}}}
Theorem. F ( J i ( α , β ) ) = F i ( K 1 ( α ) , K 2 ( β ) ) . Proof. From last theorem: F ( J i ( α , β ) ) = F i ( F ( K 1 ( J i ( α , β ) ) ) , F ( K 2 ( J i ( α , β ) ) ) ) = F i ( F ( α ) , F ( β ) ) . {\displaystyle {\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}}}
Theorem. F ( J 0 ( α , β ) ) = R n g ( F ↾ J 0 ( α , β ) ) , F ( J 1 ( α , β ) ) = { F ( α ) , F ( β ) } , F ( J 2 ( α , β ) ) = E ∩ F ( α ) , F ( J 3 ( α , β ) ) = F ( α ) ∖ F ( β ) , F ( J 4 ( α , β ) ) = F ( α ) ∩ D o m ( F ( β ) ) , F ( J 5 ( α , β ) ) = F ( α ) ∩ P v ( F ( β ) ) , F ( J 6 ( α , β ) ) = F ( α ) ∩ C p ( F ( β ) ) , F ( J 7 ( α , β ) ) = F ( α ) ∩ T r ( F ( β ) ) , Proof. Use last theorem and definition of F i ( X , Y ) . Definition. L = R n g ( F ) . {\displaystyle {\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}}}
f u n c t i o n ordinal ( x , γ ) {\displaystyle \mathbf {function} \;{\text{ordinal}}(x,\,\gamma )} i n p u t : x is a set. γ is an ordinal such that x ∈ F ( γ ) . o u t p u t : ordinal δ that satisfies: x = F ( δ ) ∧ δ < γ . {\displaystyle {\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}}}
b e g i n {\displaystyle \mathbf {begin} }
0 : i f ( x = F ( δ ) ∧ δ < γ ) // x ∈ F ( γ ) = R n g ( F ↾ γ ) implies ∃ δ ( δ < γ ∧ x = F ( δ ) ) . r e t u r n δ ; 1 : i f x = F ( α ) // α , β < γ . Also, x ∈ F ( γ ) = { F ( α ) , F ( β ) } implies x = F ( α ) ∨ x = F ( β ) . r e t u r n α ; e l s e i f x = F ( β ) r e t u r n β ; 2 , 3 , 4 , 5 , 6 , 7 : // For some class Y : x ∈ F ( γ ) = F ( α ) ∩ Y , so x ∈ F ( α ) ∧ α < γ . r e t u r n ordinal ( x , α ) ; {\displaystyle {\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}}}
e n d {\displaystyle \mathbf {end} }
Theorem. Function ordinal ( x , γ ) terminates and returns ordinal δ that satisfies: δ < γ ∧ x = F ( δ ) . Proof. All cases except the 2 , 3 , 4 , 5 , 6 , 7 terminate and return an ordinal less than the argument γ . This case does a recursive call with an argument less than γ . If the function does not terminate, it is because this case always occurs. This produces an infinite decreasing sequence of ordinals: γ > γ 1 > ⋯ > γ n > ⋯ . This contradicts the fact that there is no such decreasing sequence of ordinals. ∴ The function terminates in one of the other cases and returns a δ that satisfies: δ < γ ∧ x = F ( δ ) . {\displaystyle {\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}}}
Definition. L ( A ) ⟺ A ⊆ L ∧ ∀ x ( x ∈ L ⟹ A ∩ x ∈ L ) . That is, a class is constructible if and only if its members are constructible and the intersection with any constructible set is constructible. Definition. x ¯ , … , z ¯ will be used as variables for constructible sets and X ¯ , … , Z ¯ will be used as variables for constructible classes. Definition. The order of set x is the smallest ordinal α such that x = F ( α ) . ( x , α ) ∈ O d ⟺ ( x , α ) ∈ F ∧ ∀ β ( β ∈ α ⟹ ( x , β ) ∉ F ) ∧ O d ⊆ V 2 . {\displaystyle {\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}}}
Theorem. x ∈ F ( α ) ⟹ ∃ β ( β < α ∧ x = F ( β ) ) . Proof. See program and theorem of last section. Theorem. T r a n s ( F [ α ] ) . Proof. Let x ∈ y ∈ F [ α ] . Then x ∈ y = F ( β ) where β < α . So x ∈ F ( β ) . By the theorem above: ∃ δ ( δ < β < α ∧ x = F ( δ ) ) . ∴ x ∈ F [ α ] . Theorem. T r a n s ( L ) . Proof. Let x ∈ y ∈ L . Then y = F ( α ) for some α . So x ∈ F ( α ) . By the theorem above: ∃ β ( x = F ( β ) ) . ∴ x ∈ L . Theorem. x ∈ y ∧ x , y ∈ L ⟹ O d ( x ) < O d ( y ) . In other words, x ∈ F [ α ] ⟹ O d ( x ) < α . Proof. Let O d ( y ) = α . Then x ∈ F ( α ) , so ∃ β ( β < α ∧ x = F ( β ) ) . ∴ O d ( x ) ≤ β < α = O d ( y ) . Theorem. F i ( x ¯ , y ¯ ) ∈ L . Proof. x ¯ = F ( α ) , y ¯ = F ( β ) ⟹ F ( J i ( α , β ) ) = F i ( x ¯ , y ¯ ) . Theorem. x ¯ ∩ y ¯ ∈ L . Proof. x ¯ ∩ y ¯ = x ¯ ∖ ( x ¯ ∖ y ¯ ) = F 3 ( x ¯ , F 3 ( x ¯ , y ¯ ) ) . Theorem. x , y ∈ L ⟺ ( x , y ) ∈ L and x , y , z ∈ L ⟺ ( x , y , z ) ∈ L . Proof. x , y ∈ L ∧ ( x , y ) = { { x } , { x , y } } ⟹ ( x , y ) = F 1 ( x , F 1 ( x , y ) ) . ( x , y ) ∈ L ∧ ( x , y ) = { { x } , { x , y } } ⟹ { x , y } ∈ L ⟹ x , y ∈ L . Or use T r a n s ( L ) . By induction, true for n -tuples. Theorem. ( x , y ) ∈ L ⟺ ( y , x ) ∈ L and ( x , y , z ) ∈ L ⟺ ( z , x , y ) ∈ L ⟺ ( x , z , y ) ∈ L . Proof. By last theorem . Theorem. d o m ( x ¯ ) , t r ( x ¯ ) , c p ( x ¯ ) , t r 2 ( x ¯ ) ∈ L . Proof. By last two theorems . For example, x ¯ = ( u , v , w ) ⟹ u , v , w ∈ L ⟹ t r ( x ¯ ) = ( u , w , v ) ∈ L . {\displaystyle {\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}}}
Theorem. x ⊆ L ⟹ ∃ y ¯ ( x ⊆ y ¯ ) . Proof. Let α = l e a s t ( O n ∖ { β : ∃ u ( u ∈ x ∧ β = O d ( u ) } ) . Then y ¯ = F ( J 0 ( α , 0 ) ) = R n g ( F ↾ α ) satisfies theorem. Theorem. M ( X ¯ ) ⟹ X ¯ ∈ L . Proof. L ( X ¯ ) ⟹ X ¯ ⊆ L . M ( X ¯ ) and last theorem imply ∃ y ¯ ( X ¯ ⊆ y ¯ ) . L ( X ¯ ) ⟹ X ¯ = X ¯ ∩ y ¯ ∈ L . Theorem. L ( x ¯ ) . Proof. x ¯ ⊆ L . x ¯ ∩ y ¯ ∈ L . Theorem. x ¯ ∪ y ¯ ∈ L . Proof. x ¯ ∪ y ¯ ⊆ L ⟹ ∃ z ¯ ( x ¯ ∪ y ¯ ⊆ z ¯ ) . x ¯ ∪ y ¯ = ( x ¯ c ( z ¯ ) ∩ y ¯ c ( z ¯ ) ) c ( z ¯ ) = z ¯ ∖ ( ( z ¯ ∖ x ¯ ) ∩ ( z ¯ ∖ y ¯ ) ) . Gödel used: x ¯ ∪ y ¯ = z ¯ ∖ ( ( z ¯ ∖ x ¯ ) ∖ y ¯ ) . Theorem. ∅ ∈ L or 0 ∈ L . Proof. F ( J 0 ( 0 , 0 ) ) = R n g ( F ↾ 0 ) = ∅ . Gödel used: x ¯ ∖ x ¯ = ∅ . Theorem. L ( L ) . Proof. L ⊆ L . L ∩ x ¯ = x ¯ ∈ L . {\displaystyle {\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}}}
Theorem. L ( E ∩ L ) . Proof. E ∩ L ⊆ L . Let x ¯ = F ( α ) . Then ( E ∩ L ) ∩ x ¯ = E ∩ F ( α ) = F ( J 2 ( α , 0 ) ) ∈ L . Theorem. L ( A ¯ ∖ B ¯ ) . Proof. A ¯ ∖ B ¯ ⊆ A ¯ ⊆ L . ( A ¯ ∖ B ¯ ) ∩ x ¯ = ( A ¯ ∩ x ¯ ) ∖ ( B ¯ ∩ x ¯ ) = y ¯ ∖ z ¯ ∈ L . The last expression is the difference of two constructible sets, which is constructible by F 3 . Theorem. L ( A ¯ ∩ B ¯ ) . Proof. A ¯ ∩ B ¯ ⊆ A ¯ ⊆ L . ( A ¯ ∩ B ¯ ) ∩ x ¯ = A ¯ ∩ ( B ¯ ∩ x ¯ ) = A ¯ ∩ y ¯ ∈ L . Theorem. L ( A ¯ ∪ B ¯ ) . Proof. A ¯ ∪ B ¯ ⊆ L . ( A ¯ ∪ B ¯ ) ∩ x ¯ = ( B ¯ ∩ x ¯ ) ∪ ( A ¯ ∩ x ¯ ) = y ¯ ∪ z ¯ ∈ L . Theorem. D o m ( x ¯ ) ∈ L ; T r ( x ¯ ) ∈ L ; C p ( x ¯ ) ∈ L . Proof. Let i = d , t , or c . Q i ( x ¯ ) is a set by replacement . ∴ ∃ y ¯ ( Q i ( x ¯ ) ⊆ y ¯ ) . Let F ( α ) = y ¯ ; F ( β ) = x ¯ . Then F ( J i ( α , β ) ) = F ( α ) ∩ Q i ( F ( β ) ) = y ¯ ∩ Q i ( x ¯ ) = Q i ( x ¯ ) . ∴ Q i ( x ¯ ) ∈ L . {\displaystyle {\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}}}
Theorem. T r 2 ( x ¯ ) ∈ L . Proof. T r 2 ( x ¯ ) = D o m ( T r ( L ∩ P v ( x ¯ ) ) ) : y ∈ D o m ( T r ( L ∩ P v ( x ¯ ) ) ) ⟺ ∃ u , v , y 2 , y 3 , w ( y = ( v , u ) ∧ y 2 = ( w , v , u ) ∧ y 3 = ( w , u , v ) ∧ w ∈ L ∧ ( u , v ) ∈ x ¯ ) ⟹ y ∈ T r 2 ( x ¯ ) . y ∈ T r 2 ( x ¯ ) ⟺ ∃ u , v ( y = ( v , u ) ∧ ( u , v ) ∈ x ¯ ) ) ⟹ ∃ u , v , y 2 , y 3 , w ( y = ( v , u ) ∧ w ∈ L ∧ y 3 = ( w , u , v ) ∧ y 2 = ( w , v , u ) ∧ ( u , v ) ∈ x ¯ ) ⟺ y ∈ D o m ( T r ( L ∩ P v ( x ¯ ) ) . Theorem. R n g ( x ¯ ) ∈ L . Proof. R n g ( x ¯ ) = D o m ( T r 2 ( x ¯ ) ) : {\displaystyle {\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}}}
Theorem. L ( D o m ( A ¯ ) ) ; L ( T r ( A ¯ ) ) ; L ( C p ( A ¯ ) ) . Proof. Let i = d , t , or c . Q i ( A ¯ ) ⊆ L : v ∈ Q i ( A ¯ ) ⟹ ∃ u ( v = q i ( u ) ∧ u ∈ A ¯ ⊆ L ) . From a previous theorem: u ∈ L ⟹ q i ( u ) = v ∈ L . ∴ Q i ( A ¯ ) ⊆ L . Q i ( A ¯ ) ∩ x ¯ ∈ L : Strategy: Find a z ¯ such that Q i ( z ¯ ) ∩ x ¯ = Q i ( A ¯ ) ∩ x ¯ . Then Q i ( z ¯ ) ∩ x ¯ ∈ L since F ( J ( i , α , β ) = F i ( F ( α ) , F ( β ) ) = x ¯ ∩ Q i ( z ¯ ) . For v ∈ Q i ( A ¯ ) ∩ x ¯ , let α v = l e a s t { α : u ∈ A ¯ ∧ v = q i ( u ) ∧ u = F ( α ) } . Let y = { F ( α v ) : v ∈ x ¯ } , which is a set by replacement. Let ∃ b ¯ ( y ⊆ b ¯ ) . Let z ¯ = A ¯ ∩ b ¯ . Then y ⊆ z ¯ ⊆ A ¯ . z ¯ ⊆ A ¯ ⟹ Q i ( z ¯ ) ∩ x ¯ ⊆ Q i ( A ¯ ) ∩ x ¯ . v ∈ Q i ( A ¯ ) ∩ x ¯ ⟹ ∃ u ( u ∈ A ¯ ∧ v = q i ( u ) ) ⟹ u = F ( α v ) ⟹ u ∈ y ⟹ u ∈ z ¯ ⟹ v ∈ Q ( z ¯ ) . Hence, v ∈ Q i ( z ¯ ) ∩ x ¯ . So Q i ( A ¯ ) ∩ x ¯ ⊆ Q ( z ¯ ) ∩ x ¯ . ∴ Q i ( A ¯ ) ∩ x ¯ = Q i ( z ¯ ) ∩ x ¯ ∈ L . Theorem. L ∩ ( V × A ¯ ) = L × A ¯ . Proof. x ∈ L ∩ ( V × A ¯ ) ⟺ x ∈ L ∧ x = ( u , v ) ∧ u ∈ V ∧ v ∈ A ¯ . ⟺ x = ( u , v ) ∧ u , v ∈ L ∧ v ∈ A ¯ ⟺ x = ( u , v ) ∧ u ∈ L ∧ v ∈ A ¯ ⟺ x ∈ L × A ¯ . Theorem. L ( L ∩ P v ( A ¯ ) ) or L ( L ∩ ( V × A ¯ ) ) or L ( L × A ¯ ) ) . Proof. L ∩ P v ( A ¯ ) ⊆ L . ( L ∩ P v ( A ¯ ) ) ∩ x ¯ ∈ L : In last proof: replace Q i ( A ¯ ) with L ∩ P v ( A ¯ ) . ( L ∩ P v ( A ¯ ) ) ∩ x ¯ ∈ L : Strategy: Find a z ¯ such that P v ( z ¯ ) ∩ x ¯ = ( L ∩ P v ( A ¯ ) ) ∩ x ¯ . Then P v ( z ¯ ) ∩ x ¯ ∈ L since F ( J ( v , α , β ) = F v ( F ( α ) , F ( β ) ) = x ¯ ∩ P v ( z ¯ ) . For v ∈ ( L ∩ P v ( A ¯ ) ) ∩ x ¯ , let α v = l e a s t { α : u ∈ A ¯ ∧ ∃ w ( v = ( w , u ) ∧ u = F ( α ) } . Let y = { F ( α v ) : v ∈ x ¯ } , which is a set by replacement. Let ∃ b ¯ ( y ⊆ b ¯ ) . Let z ¯ = ( L ∩ P v ( A ¯ ) ) ∩ b ¯ . Then y ⊆ z ¯ ⊆ ( L ∩ P v ( A ¯ ) ) . z ¯ ⊆ ( L ∩ P v ( A ¯ ) ) ⟹ Q i ( z ¯ ) ∩ x ¯ ⊆ ( L ∩ P v ( A ¯ ) ) ∩ x ¯ . v ∈ ( L ∩ P v ( A ¯ ) ) ∩ x ¯ ⟹ ∃ u ( u ∈ A ¯ ∧ ∃ w ( v = ( w , u ) ) ) . ⟹ u = F ( α v ) ⟹ u ∈ y ⟹ u ∈ z ¯ ⟹ v ∈ Q ( z ¯ ) . Hence, v ∈ P v ( z ¯ ) ∩ x ¯ . So ( L ∩ P v ( A ¯ ) ) ∩ x ¯ ⊆ Q ( z ¯ ) ∩ x ¯ . ∴ ( L ∩ P v ( A ¯ ) ) ∩ x ¯ = P v ( z ¯ ) ∩ x ¯ ∈ L . Theorem. L ( T r 2 ( A ¯ ) ) . Proof. T r 2 ( A ¯ ) = D o m ( T r ( L ∩ P v ( A ¯ ) ) ) . L ( L ∩ P v ( A ¯ ) ) ⟹ L ( T r ( L ∩ P v ( A ¯ ) ) ⟹ L ( D o m ( T r ( L ∩ P v ( A ¯ ) ) ) ⟹ L ( T r 2 ( A ¯ ) ) . Theorem. L ( A ¯ × B ¯ ) . Proof. ( A ¯ × L ) ∩ ( L × B ¯ ) = ( A ¯ ∩ L ) × ( L ∩ B ¯ ) = A ¯ × B ¯ . By a previous theorem: L ( L × B ¯ ) . Now A ¯ × L = T r 2 ( L × A ¯ ) ⟹ L ( A ¯ × L ) . ∴ L ( ( A ¯ × L ) ∩ ( L × B ¯ ) ) or L ( A ¯ × B ¯ ) . Theorem. L ( R n g ( A ¯ ) ) . Proof. R n g ( ( A ¯ ) = D o m ( T r 2 ( ( A ¯ ) ) ) so result follows from: L ( T r 2 ( A ¯ ) ) , L ( D o m ( A ¯ ) ) . {\displaystyle {\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}}}
Theorem. L ( A ¯ ↾ B ¯ ) . Proof. A ¯ ↾ B ¯ = A ¯ ∩ ( V × B ¯ ) = A ¯ ∩ L ∩ ( V × B ¯ ) = A ¯ ∩ ( L × B ¯ ) , so result follows from: L ( L × B ¯ ) , L ( A ¯ ∩ B ¯ ) . Theorem. L ( A ¯ [ B ¯ ] ) . Proof. A ¯ [ B ¯ ] = R n g ( A ¯ ↾ B ¯ ) so result follows from: L ( A ¯ ↾ B ¯ ) , L ( R n g ( A ¯ ) ) . Theorem. L ( { X ¯ , Y ¯ } ) . Proof. By definition of ordered pair for classes: { X ¯ , Y ¯ } = ∅ , { X ¯ } , { Y ¯ } , or { X ¯ , Y ¯ } where only sets appear in braces. Theorem follows from preceding theorems. {\displaystyle {\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}}}
Absoluteness theorems. These theorems are used to prove absoluteness. A b s 1 : [ ∀ u ( P ( u ) ⟹ Q ( u ) ) ∧ ( P ( u ) ⟹ u ∈ L ) ] ⟺ ∀ u ¯ ( P ( u ¯ ) ⟹ Q ( u ¯ ) ) . A b s 2 : [ ∀ u ( P ( u ) ⟺ Q ( u ) ) ∧ ( P ( u ) ⟹ u ∈ L ) ∧ ( Q ( u ) ⟹ u ∈ L ) ] ⟺ ∀ u ¯ ( P ( u ¯ ) ⟺ Q ( u ¯ ) ) . A b s 3 : [ ∀ u ∀ v ∀ w ( P ( u , v , w ) ⟹ Q ( u , v , w ) ) ∧ ( P ( u , v , w ) ⟹ u , v , w ∈ L ) ] ⟺ ∀ u ¯ ∀ v ¯ ∀ w ¯ ( P ( u ¯ , v ¯ , w ¯ ) ⟹ Q ( u ¯ , v ¯ , w ¯ ) ) . Proof. ⟹ direction: ∀ u ( P ( u ) ⟹ Q ( u ) ) ⟹ ∀ u ( u ∈ L ⟹ ( P ( u ) ⟹ Q ( u ) ) ) ⟺ ∀ u ¯ ( P ( u ¯ ) ⟹ Q ( u ¯ ) ) . ∀ u ( P ( u ) ⟺ Q ( u ) ) ⟹ ∀ u ( u ∈ L ⟹ ( P ( u ) ⟺ Q ( u ) ) ) ⟺ ∀ u ¯ ( P ( u ¯ ) ⟺ Q ( u ¯ ) ) . ⟸ direction: Case 1: u ∈ L . ∀ u ¯ ( P ( u ¯ ) ⟹ Q ( u ¯ ) ) ⟺ ∀ u ( u ∈ L ⟹ ( P ( u ) ⟹ Q ( u ) ) ) , so u ∈ L implies P ( u ) ⟹ Q ( u ) . ∀ u ¯ ( P ( u ¯ ) ⟺ Q ( u ¯ ) ) ⟺ ∀ u ( u ∈ L ⟹ ( P ( u ) ⟺ Q ( u ) ) ) , so u ∈ L implies P ( u ) ⟺ Q ( u ) . Case 2: u ∉ L . ∀ u ( u ∉ L ⟹ ¬ P ( u ) ) , so u ∉ L implies P ( u ) ⟹ Q ( u ) . ∀ u ( u ∉ L ⟹ ¬ P ( u ) ∧ ¬ Q ( u ) ) , so u ∉ L implies P ( u ) ⟺ Q ( u ) . Putting both cases together: ∀ u ¯ ( P ( u ¯ ) ⟹ Q ( u ¯ ) ) ⟹ ∀ u ( P ( u ) ⟹ Q ( u ) ) . ∀ u ¯ ( P ( u ¯ ) ⟺ Q ( u ¯ ) ) ⟹ ∀ u ( P ( u ) ⟺ Q ( u ) ) . {\displaystyle {\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}}}
Theorem. X ¯ ⊆ Y ¯ ⟺ X ¯ ⊆ l Y ¯ . Proof. X ¯ ⊆ l Y ¯ ⟺ ∀ u ¯ ( u ¯ ∈ X ¯ ⟹ u ¯ ∈ Y ¯ ) . X ¯ ⊆ Y ¯ ⟺ ∀ u ( u ∈ X ¯ ⟹ u ∈ Y ¯ ) ⟺ ∀ u ¯ ( u ¯ ∈ X ¯ ⟹ u ¯ ∈ Y ¯ ) by A b s 1 since u ∈ X ¯ ⟹ u ∈ L . ⟺ X ¯ ⊆ l Y ¯ . Theorem. X ¯ = Y ¯ ⟺ ∀ u ¯ ( u ¯ ∈ X ¯ ⟺ u ¯ ∈ Y ¯ ) . Constructive extensionality: Two constructive classes are equal iff they have the same constructible elements. Proof. X ¯ = Y ¯ ⟺ ∀ u ( u ∈ X ¯ ⟺ u ∈ Y ¯ ) ⟺ ∀ u ¯ ( u ¯ ∈ X ¯ ⟹ u ¯ ∈ Y ¯ ) by A b s 2 since u ∈ X ¯ and u ∈ Y ¯ ⟹ u ∈ L . Theorem. { X ¯ , Y ¯ } l = { X ¯ , Y ¯ } . Proof. ∀ u ¯ ( u ¯ ∈ { X ¯ , Y ¯ } l ⟺ u ¯ = X ¯ ∨ u ¯ = Y ¯ ) . A previous theorem proved that { X ¯ , Y ¯ } ∈ L . Using A b s 2 since u ∈ { X ¯ , Y ¯ } ⟹ u ∈ L and u = X ¯ ∨ u = Y ¯ ⟹ u ∈ L : ∀ u ( u ∈ { X ¯ , Y ¯ } ⟺ u = X ¯ ∨ u = Y ¯ ) ⟺ ∀ u ¯ ( u ¯ ∈ { X ¯ , Y ¯ } ⟺ u ¯ = X ¯ ∨ u ¯ = Y ¯ ) , ∴ { X ¯ , Y ¯ } l = { X ¯ , Y ¯ } by constructive extensionality. Theorem. If A , B are absolute, then A l ( B l ( X ¯ ) ) = A ( B ( X ¯ ) ) . Proof. Since A is absolute and B l ( X ¯ ) is constructive, and B is absolute: A l ( B l ( X ¯ ) ) = A ( B l ( X ¯ ) ) = A ( B ( X ¯ ) ) . Theorem. ( X ¯ , Y ¯ ) l = ( X ¯ , Y ¯ ) . (An example of last proof.) Proof. ( X ¯ , Y ¯ ) l = { { X ¯ } l , { X ¯ , Y ¯ } l } l = { { X ¯ } l , { X ¯ , Y ¯ } l } = { { X ¯ } , { X ¯ , Y ¯ } } = ( X ¯ , Y ¯ ) . Theorem. If n A , … , 1 A are absolute, then n A l ( ⋯ ( 1 A l ( X ¯ ) ) = n A ( ⋯ ( 1 A ( X ¯ ) ) . Proof. Basis step: 1 A l ( X ¯ ) = 1 A ( X ¯ ) . Inductive step: Assume n A l ( ⋯ ( 1 A l ( X ¯ ) ) = n A ( ⋯ ( 1 A ( X ¯ ) ) . Then: n + 1 A l ( n A l ( ⋯ ( 1 A l ( X ¯ ) ) ) = n + 1 A ( n A l ( ⋯ ( 1 A l ( X ¯ ) ) ) = n + 1 A ( n A ( ⋯ ( 1 A ( X ¯ ) ) ) . {\displaystyle {\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}}}
Theorem. M l ( X ¯ ) ⟺ M ( X ¯ ) . Proof. M l ( X ¯ ) ⟺ X ¯ ∈ L . X ¯ ∈ L ⟹ M ( X ¯ ) by axiom A2. M ( X ¯ ) ⟹ X ¯ ∈ L by a previous theorem. Thus, X ¯ ∈ L ⟺ M ( X ¯ ) . ∴ M l ( X ¯ ) ⟺ M ( X ¯ ) . Theorem. P r l ( X ¯ ) ⟺ P r ( X ¯ ) . Proof. P r l ( X ¯ ) ⟺ ¬ M l ( X ¯ ) ⟺ ¬ M ( X ¯ ) ⟺ P r ( X ¯ ) . Theorem. V l = L . Proof. ∀ u ¯ ( u ¯ ∈ V l ) . ∀ u ¯ ( u ¯ ∈ L ) . Hence, ∀ u ¯ ( u ¯ ∈ V l ⟺ u ¯ ∈ L ) . Since L is constructive, V l = L by constructive extensionality. Theorem. ∅ is absolute . Proof. ∀ u ( u ∉ ∅ ) ⟹ ∀ u ¯ ( u ¯ ∉ ∅ ) . Also, ∀ u ¯ ( u ¯ ∉ ∅ l ) . Since ∅ is constructive, ∅ l = ∅ by constructive extensionality. Theorem. U n l ( F ¯ ) ⟺ U n ( F ¯ ) . Proof. U n l ( F ¯ ) ⟺ ∀ u ¯ ∀ v ¯ ∀ w ¯ ( ( v ¯ , u ¯ ) ∈ F ¯ ∧ ( w ¯ , u ¯ ) ∈ F ¯ ⟹ v ¯ = w ¯ ) . U n ( F ¯ ) ⟺ ∀ u ∀ v ∀ w ( ( v , u ) ∈ F ¯ ∧ ( w , u ) ∈ F ¯ ⟹ v = w ) . ⟺ ∀ u ¯ ∀ v ¯ ∀ w ¯ ( ( v ¯ , u ¯ ) ∈ F ¯ ∧ ( w ¯ , u ¯ ) ∈ F ¯ ⟹ v ¯ = w ¯ ) by A b s 3 since ( v , u ) ∈ F ¯ ∧ ( w , u ) ∈ F ¯ ⟹ u , v , w ∈ L ⟺ U n l ( F ¯ ) . Theorem. ∪ l x ¯ = ∪ x ¯ . Proof. ∀ u ¯ ( u ¯ ∈ ∪ l x ¯ ⟺ ∃ v ¯ ( u ¯ ∈ v ¯ ∧ v ¯ ∈ x ¯ ) ) . Strategy: form the set { ( u , v ) ∈ E ∩ ( L × x ¯ ) } . Then replace L with a set. ∪ x ¯ ⊆ w ¯ . Let z ¯ = D o m ( E ∩ ( w ¯ × x ¯ ) ) . u ∈ z ¯ ⟺ u ∈ D o m ( E ∩ ( w ¯ × x ¯ ) ) ⟺ ∃ v ( ( u , v ) ∈ E ∧ ( u , v ) ∈ w ¯ × x ¯ ) ⟺ ∃ v ( u ∈ v ∧ u ∈ w ¯ ∧ v ∈ x ¯ ) ⟺ ∃ v ( u ∈ v ∧ v ∈ x ¯ ) (Since ∃ v ( u ∈ v ∧ v ∈ x ¯ ) ⟹ u ∈ ∪ x ¯ ⊆ w ¯ ) . ⟺ u ∈ ∪ x ¯ and ⟺ ∃ v ¯ ( u ¯ ∈ v ¯ ∧ v ¯ ∈ x ¯ ) ⟺ u ¯ ∈ ∪ l x ¯ . {\displaystyle {\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}}}
A 1 l : L ( x ¯ ) . Proof. A previous theorem. A 2 l : X ¯ ∈ Y ¯ ⟹ M l ( X ¯ ) . Proof. Using A2 and absoluteness of M : X ¯ ∈ Y ¯ ⟹ M ( X ¯ ) ⟹ M l ( X ¯ ) . A 3 l : ∀ u ¯ ( u ¯ ∈ X ¯ ⟺ u ¯ ∈ Y ¯ ) ⟹ X ¯ = Y ¯ . Proof. By constructive extensionality. A 4 l : ∀ x ¯ ∀ y ¯ ∃ z ¯ ∀ u ¯ ( u ¯ ∈ z ¯ ⟺ u ¯ = x ¯ ∨ u ¯ = y ¯ ) . Proof. Let z ¯ = { x ¯ , y ¯ } , and use absoluteness of pairing operation. {\displaystyle {\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}}}
B 1 l : ∃ E ¯ ∀ u ¯ ∀ v ¯ ( ( u ¯ , v ¯ ) ∈ E ¯ ⟺ u ¯ ∈ v ¯ ) . Proof. Using B1, there exists an E : ∀ u ∀ v ( ( u , v ) ∈ E ⟺ u ∈ v ) . Let E ¯ = E ∩ L . By a previous theorem: L ( E ∩ L ) . ( u ¯ , v ¯ ) ∈ E ¯ ⟹ ( u ¯ , v ¯ ) ∈ E ⟹ u ¯ ∈ v ¯ . u ¯ ∈ v ¯ ⟹ ( u ¯ , v ¯ ) ∈ E . Also, ( u ¯ , v ¯ ) ∈ L . Thus, u ¯ ∈ v ¯ ⟹ ( u ¯ , v ¯ ) ∈ E ∩ L = E ¯ . ∴ ∀ u ¯ ∀ v ¯ ( ( u ¯ , v ¯ ) ∈ E ¯ ⟺ u ¯ ∈ v ¯ ) . B 2 l : ∀ A ¯ ∀ B ¯ ∃ C ¯ ∀ u ¯ ( u ¯ ∈ C ¯ ⟺ u ¯ ∈ A ¯ ∧ u ¯ ∈ B ¯ ) . Proof. Using B2, let C ¯ = A ¯ ∩ B ¯ . By a previous theorem: L ( A ¯ ∩ B ¯ ) . B2 implies ∀ u ( u ∈ C ¯ ⟺ u ∈ A ¯ ∧ u ∈ B ¯ ) . ∴ ∀ u ¯ ( u ¯ ∈ C ¯ ⟺ u ¯ ∈ A ¯ ∧ u ¯ ∈ B ¯ ) . We can also prove that ∩ l is absolute, but this is not needed here. B 3 l : ∀ A ¯ ∃ B ¯ ∀ u ¯ ( u ¯ ∈ B ¯ ⟺ u ¯ ∉ A ¯ ) . Proof. Let B ¯ = L ∖ A ¯ . By a previous theorem: L ( L ∖ A ¯ ) . ∀ u ( u ∈ B ¯ ⟺ u ∈ L ∧ u ∉ A ¯ ) . ∴ u ¯ ( u ¯ ∈ B ¯ ⟺ u ¯ ∈ L ∧ u ¯ ∉ A ¯ ⟺ u ¯ ∉ A ¯ ) . B 4 l : ∀ A ¯ ∃ B ¯ ∀ u ¯ ( u ¯ ∈ B ¯ ⟺ ∃ v ¯ ( ( v ¯ , u ¯ ) ∈ A ¯ ) . Proof. Let B ¯ = D o m ( A ¯ ) . By a previous theorem: L ( D o m ( A ¯ ) ) . ∀ u [ u ∈ B ¯ ⟺ ∃ v ( ( v , u ) ∈ A ¯ ) ] . ∴ ∀ u ¯ [ u ¯ ∈ B ¯ ⟺ ∃ v ( ( v , u ¯ ) ∈ A ¯ ) ⟺ ∃ v ¯ ( ( v ¯ , u ¯ ) ∈ A ¯ ) ] . B 5 l : ∀ A ¯ ∃ B ¯ ∀ u ¯ ∀ v ¯ ( ( v ¯ , u ¯ ) ∈ B ¯ ⟺ u ¯ ∈ A ¯ ) . Proof. Let B ¯ = L × A ¯ . By a previous theorem: L ( L × A ¯ ) . ∀ u ∀ v [ ( v , u ) ∈ B ¯ ⟺ ( v ¯ ∈ L ∧ u ¯ ∈ A ¯ ) ] . ∴ ∀ u ¯ ∀ v ¯ [ ( v ¯ , u ¯ ) ∈ B ¯ ⟺ ( v ¯ ∈ L ∧ u ¯ ∈ A ¯ ) ⟺ u ¯ ∈ A ¯ ] . B 6 l : ∀ A ¯ ∃ B ¯ ∀ u ¯ ∀ v ¯ ∀ w ¯ ( ( u ¯ , v ¯ , w ¯ ) ∈ B ¯ ⟺ ( v ¯ , u ¯ , w ¯ ) ∈ A ¯ ) . Proof. Let B ¯ = T r ( A ¯ ) . By a previous theorem: L ( T r ( A ¯ ) ) . ∀ u ∀ u ∀ w [ ( u , v , w ) ∈ B ¯ ⟺ ( v , u , w ) ∈ A ¯ ] . ∴ ∀ u ¯ ∀ v ¯ ∀ w ¯ [ ( u ¯ , v ¯ , w ¯ ) ∈ B ¯ ⟺ ( v ¯ , u ¯ , w ¯ ) ∈ A ¯ ] . B 7 l : ∀ A ¯ ∃ B ¯ ∀ u ¯ ∀ v ¯ ∀ w ¯ ( ( w ¯ , u ¯ , v ¯ ) ∈ B ¯ ⟺ ( u ¯ , v ¯ , w ¯ ) ∈ A ¯ ) . Proof. Let B ¯ = C p ( A ¯ ) . By a previous theorem: L ( C p ( A ¯ ) ) . ∀ u ∀ u ∀ w [ ( w , u , v ) ∈ B ¯ ⟺ ( u , v , w ) ∈ A ¯ ] . ∴ ∀ u ¯ ∀ v ¯ ∀ w ¯ [ ( w ¯ , u ¯ , v ¯ ) ∈ B ¯ ⟺ ( u ¯ , v ¯ , w ¯ ) ∈ A ¯ ] . {\displaystyle {\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}}}
C 1 l : ∃ a ¯ [ ¬ E m ( a ¯ ) ∧ ∀ x ¯ ( x ¯ ∈ a ¯ ⟹ ∃ y ¯ ( y ¯ ∈ a ¯ ∧ x ¯ ⊂ y ¯ ) ) ] . Proof. Let a ¯ = F ( J ( 0 , ω , 0 ) ) . ( i , α , β ) S ( 0 , ω , 0 ) ⟹ ( α , β ) R ( ω , 0 ) ∨ ( ( α , β ) = ( ω , 0 ) ∧ i < 0 [latter disjunct cannot occur.] ( α , β ) R ( ω , 0 ) ⟺ M a x ( α , β ) < M a x ( ω , 0 ) ∨ ( M a x ( α , β ) = M a x ( ω , 0 ) ∧ ( α , β ) L e ( ω , 0 ) . ) ( α , β ) L e ( ω , 0 ) ⟺ β < 0 ∨ ( β = 0 ∧ α < ω ) . Last two cases imply: α , β < ω . ∴ x ¯ ∈ a ¯ ⟹ x ¯ = F ( J ( i , α , β ) ) < F ( J ( 0 , ω , 0 ) ) ⟹ α , β < ω ⟹ J ( i , α , β ) = n < ω . ∅ ∈ a ¯ ⟹ ¬ E m ( a ¯ ) . We now prove x ¯ ∈ a ¯ ⟹ x ¯ ∪ { x ¯ } ∈ a ¯ : x ¯ ∈ a ¯ ⟹ ∃ n < ω ( x ¯ = F ( n ) ) . Then { x ¯ } = { x ¯ , x ¯ } = F ( J ( ( p , n , n ) ) = F ( J ( n 1 ) ) . x ¯ ∪ { x ¯ } ⊆ z ¯ = F ( J ( ( 0 , n 1 + 1 , 0 ) ) ) . Then x ¯ ∪ { x ¯ } = z ¯ ∖ ( z ∖ x ¯ ) ∖ { x ¯ } ) = F ( n 2 ) ∈ F ( J ( ( 0 , ω , 0 ) ) ) . Let y ¯ = x ¯ ∪ { x ¯ } . ∴ y ¯ ∈ a ¯ ∧ x ¯ ⊂ y ¯ . {\displaystyle {\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}}}
Definition. ( α , β ) L e ( γ , δ ) ⟺ β < δ ∨ ( β = δ ∧ α < γ ) . Definition. ( α , β ) R ( γ , δ ) ⟺ M a x ( α , β ) < M a x ( γ , δ ) ∨ ( M a x ( α , β ) = M a x ( γ , δ ) ∧ ( α , β ) L e ( γ , δ ) ) Definition. ( i , α , β ) S ( j , γ , δ ) ⟺ ( α , β ) R ( γ , δ ) ∨ ( ( α , β ) = ( γ , δ ) ∧ i < j . {\displaystyle {\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}}}
C 2 l : ∀ x ¯ ∃ y ¯ ∀ u ¯ ∀ v ¯ [ ( u ¯ ∈ v ¯ ∧ v ¯ ∈ x ¯ ) ⟹ u ¯ ∈ y ¯ ] . Proof. Using axiom C2: Let y satisfy ∀ u ∀ v ( u ∈ v ∧ v ∈ x ¯ ⟹ u ∈ y ) . Since L ∩ y ⊆ L , there is a z ¯ such that L ∩ y ⊆ z ¯ . z ¯ satisfies C 2 l : ( u ¯ ∈ v ¯ ∧ v ¯ ∈ x ¯ ) ⟹ u ¯ ∈ y ⟹ u ¯ ∈ L ∩ y ⟹ u ¯ ∈ z ¯ . C 3 l : ∀ x ¯ ∃ y ¯ ∀ u ¯ [ ( u ¯ ⊆ x ¯ ⟹ u ¯ ∈ y ¯ ] . Proof. Using axiom C3: Let y satisfy ∀ u ( u ⊆ x ¯ ⟹ u ∈ y ) . Since L ∩ y ⊆ L , there is a z ¯ such that L ∩ y ⊆ z ¯ . z ¯ satisfies C 3 l : u ¯ ⊆ x ¯ ⟹ u ¯ ∈ y ⟹ u ¯ ∈ L ∩ y ⟹ u ¯ ∈ z ¯ . C 4 l : ∀ x ¯ ∀ F ¯ [ U n ( F ¯ ) ⟹ ∃ y ¯ ∀ v ¯ ( v ¯ ∈ y ¯ ⟺ ∃ u ¯ ( u ¯ ∈ x ¯ ) ∧ ( v ¯ , u ¯ ) ∈ F ¯ ) ] . Proof. Using axiom C4: Given x ¯ and F ¯ , there is a y such that ∀ v ( v ∈ y ⟺ ∃ u ( u ∈ x ¯ ∧ ( v , u ) ∈ F ¯ ) ) . Now y = F ¯ [ x ¯ ] ⟹ M ( F ¯ [ x ¯ ] ) . By a previous theorem, L ( F ¯ [ x ¯ ] ) . ∴ y ∈ L . Since ( v ∈ y ⟹ v ∈ L ) ∧ ( u ∈ x ¯ ⟹ u ∈ L ) , we have: ∃ y ¯ ∀ v ¯ ( v ¯ ∈ y ¯ ⟺ ∃ u ¯ ( u ¯ ∈ x ¯ ) ∧ ( v ¯ , u ¯ ) ∈ F ¯ ) . *********** CHECK NEXT 2: HAVE WE STATED D1 and E1 correctly?? D 1 l : ¬ E m ( A ¯ ) ⟹ ∃ u ¯ [ u ¯ ∈ A ¯ ∧ E x ( u ¯ , A ¯ ) ] . Proof. Let ¬ E m ( A ¯ ) . Using axiom D1: Let u satisfy u ∈ A ¯ ∧ E x ( u , A ¯ ) ) . Since u ∈ A ¯ ⟹ u ∈ L , we have: ∃ u ¯ [ u ¯ ∈ A ¯ ∧ E x ( u ¯ , A ¯ ] . E 1 l : ∃ G ¯ ∀ x ¯ [ U n ( G ¯ ) ∧ ∃ y ¯ ( ¬ E m ( x ¯ ) ⟹ ( y ¯ , x ¯ ) ∈ G ¯ ) ] . Proof. Define: ( y ¯ , x ¯ ) ∈ G ¯ ⟺ y ¯ ∈ x ¯ ∧ ∀ z ¯ ( O d ( y ¯ ) ≤ O d ( z ¯ ) ) . Must prove: L ( G ¯ ) . Follows from Class Existence Theorem, but must prove that Od is absolute. {\displaystyle {\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}}}
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/19d09d833efb541b0ce1413e0d00436feab4ce67)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1237de40cf8acdfacccebd7443a3e5d56e6512b3)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4a2cc6924d2f8069ab9a788cbe79be6bd89f4e36)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b9f49e14809d8b990ac7d1399da00c90e283fc6f)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e87b40e6f4103597501b2cbcaedfdd299d98e7bb)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea85e47ef00683dac56ce0bf80511d539748a386)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fa19f47b92218417a2a8bab5eb685d1156ff82d8)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d82a5bea5da329fc873f4d3b52fbd368cb8105a7)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ffb59290527ecb2354e0532b57c79b439dedff5f)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb95a84a817158221bee515fa0e1c3ee5852e381)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d687f5b32a283cfac315e89cad9b4449794a4e0)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ac3fd15589469b4147cd7a7523f2cab99ed9955)
