avewright/proofwiki-math huggingface dataset:
Theorem: G-Tower is Properly Well-Ordered under Subset Relation

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Then $M$ is properly well-ordered under the subset relation.

Proof:
From $g$-Tower is Well-Ordered under Subset Relation, $\subseteq$ is a well-ordering on $M$.
Let $L$ be a proper lower section of $M$.
From Proper Lower Section under Well-Ordering is Initial Segment, $L$ is an initial segment $x^\subset$ of $M$ for some $x \in M$.
By the definition of the structure of a $g$-tower, each element of $x$ is a subset of $x$.
Hence:
:$x^\subset \subseteq \powerset x$
From the Axiom of Powers, $\powerset x$ is a set.
Hence from Subclass of Set is Set, $x^\subset$ is also a set.
The result follows from the definition of properly well-ordered.
{{qed}}
Theorem: Extension of Contraction of Extension of Ideal is Extension

Let $A$ and $B$ be commutative rings with unity.
Let $f : A \to B$ be a ring homomorphism.
Let $\mathfrak a$ be an ideal of $A$.
Let ${\mathfrak a}^e$ be the extension of $\mathfrak a$ by $f$.
Let ${\mathfrak a}^{ec}$ be the contraction of ${\mathfrak a}^e$ by $f$.
Let ${\mathfrak a}^{ece}$ be the extension of ${\mathfrak a}^{ec}$ by $f$.
Then:
:${\mathfrak a}^e = {\mathfrak a}^{ece}$

Proof:
Since $\mathfrak a \subseteq {\mathfrak a}^{ec}$ by Ideal is Contained in Contraction of Extension:
{{begin-eqn}}
{{eqn | l = {\mathfrak a}^e
      | r = \paren { {\mathfrak a}^{ec} }^e
      | o = \subseteq
      | c = Extension of Ideals Preserves Inclusion Order }}
{{eqn | r = {\mathfrak a}^{ece}
      | c = Composition of Mappings is Associative }}
{{eqn | r = \paren { {\mathfrak a}^e }^{ce}
      | c = Composition of Mappings is Associative }}
{{eqn | r = {\mathfrak a}^e
      | o = \subseteq
      | c = Ideal Contains Extension of Contraction }}
{{end-eqn}}
{{qed}}
Category:Ideal Theory
Category:Commutative Algebra
Category:Ring Theory
ockifq9h2k6s50fbgp31pcxywkfohuv
Theorem: Contraction of Extension of Contraction of Ideal is Contraction

Let $A$ and $B$ be commutative rings with unity.
Let $f : A \to B$ be a ring homomorphism.
Let $\mathfrak b$ be an ideal of $B$.
Let ${\mathfrak b}^c$ be the contraction of $\mathfrak b$ by $f$.
Let ${\mathfrak b}^{ce}$ be the extension of ${\mathfrak b}^c$ by $f$.
Let ${\mathfrak b}^{cec}$ be the contraction of ${\mathfrak b}^{ce}$ by $f$.
Then:
:${\mathfrak b}^c = {\mathfrak b}^{cec}$

Proof:
Since $\mathfrak b \supseteq {\mathfrak b}^{ce}$ by Ideal Contains Extension of Contraction:
{{begin-eqn}}
{{eqn | l = {\mathfrak b}^c
      | r = \paren { {\mathfrak b}^{ce} }^c
      | o = \supseteq
      | c = Contraction of Ideals Preserves Inclusion Order
}}
{{eqn | r = {\mathfrak b}^{cec}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = \paren { {\mathfrak b}^c}^{ec}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = {\mathfrak b}^c
      | o = \supseteq
      | c = Ideal is Contained in Contraction of Extension
}}
{{end-eqn}}
{{qed}}
Category:Ideal Theory
Category:Commutative Algebra
Category:Ring Theory
ry9qdjpq772n739i2mjg9296u8ydaqa
Theorem: Measure-Preserving Transformation Preserves Conditional Entropy

Let $\struct {X, \BB, \mu}$ be a probability space.
Let $T: X \to X$ be a $\mu$-preserving transformation.
Let $\AA, \DD \subseteq \Sigma$ be finite sub-$\sigma$-algebras.
Then:
:$\map H {T^{-1} \AA \mid T^{-1} \DD} = \map H {\AA \mid \DD}$
where:
:$\map H {\cdot \mid \cdot}$ denotes the conditional entropy
:$T^{-1} \AA$ is the pre-image $\sigma$-algebra of $\AA$ on the domain of $T$
:$T^{-1} \DD$ is the pre-image $\sigma$-algebra of $\DD$ on the domain of $T$

Proof:
By {{Defof|Finite Partition Generated by Finite Sub-Sigma-Algebra}}, we have:
:$\map \xi {T^{-1} \AA} = T^{-1} {\map \xi \AA}$
for each finite sub-$\sigma$-algebras $\AA \subseteq \Sigma$.
Thus it suffices to show that the entropy of finite partition satisfies:
:$\map H {T^{-1} \xi \mid T^{-1} \eta} = \map H {\xi \mid \eta}$
for all $\xi, \eta$ be finite partitions of $\Omega$.
Now:
{{begin-eqn}}
{{eqn | l = \map H {T^{-1} \xi \mid T^{-1} \eta}
      | r = \sum_{\substack {B \mathop \in \eta \\ \map \mu {T^{-1} B} \mathop > 0} } \map \mu {T^{-1} B} \sum_{A \mathop \in \xi} \map \phi {\dfrac {\map \mu {T^{-1} A \cap T^{-1} B} } {\map \mu {T^{-1} B} } }
      | c = {{Defof|Conditional Entropy of Finite Partitions}}
}}
{{eqn | r = \sum_{\substack {B \mathop \in \eta \\ \map \mu B \mathop > 0} } \map \mu B \sum_{A \mathop \in \xi} \map \phi {\dfrac {\map \mu {A \cap B} } {\map \mu B } }
      | c = since $T$ is $\mu$-preserving
}}
{{eqn | r = \map H {\xi \mid \eta}
      | c = {{Defof|Conditional Entropy of Finite Partitions}}
}}
{{qed}}
Category:Probability Theory
Category:Ergodic Theory
izbbgy10zd0d3k8mcthrg8neqvseew1
Theorem: Union of Nest of Mappings is Mapping

Let $N$ be a nest of mappings.
Then:
:$\bigcup N$ is a mapping
where $\bigcup N$ denotes the union of $N$.

Proof:
By definition of union, the elements of $\bigcup N$ are elements of elements of $N$.
That is, the elements of $\bigcup N$ are ordered pairs of sets.
Let $x \in \bigcup N$.
Then:
:$\exists f \subseteq \bigcup N: \exists y: \tuple {x, y} \in f$
{{AimForCont}}:
:$\exists y_1, y_2: \tuple {x, y_1} \in \bigcup N \land \tuple {x, y_2} \in \bigcup N$
such that:
:$y_1 \ne y_2$
Then:
:$\exists f \subseteq \bigcup N: \tuple {x, y_1} \in f$
and:
:$\exists g \subseteq \bigcup N: \tuple {x, y_2} \in g$
But because $N$ is a nest of mappings, either:
:$f \subseteq g$
or:
:$g \subseteq f$
That means either:
:$\tuple {x, y_1} \in g$
or:
:$\tuple {x, y_2} \in f$
Hence either $f$ or $g$ has both $\tuple {x, y_1}$ and $\tuple {x, y_2}$ in it.
That is, either $f$ or $g$ is not a mapping.
From this contradiction it follows that if: 
:$\exists y_1, y_2: \tuple {x, y_1} \in \bigcup N \land \tuple {x, y_2} \in \bigcup N$
then it has to be the case that:
:$y_1 = y_2$
It follows that $\bigcup N$ is a mapping.
{{qed}}
Theorem: Domain of Union of Nest of Mappings is Union of Class of Domains

Let $N$ be a nest of mappings.
Let $\bigcup N$ denote the union of $N$.
Then:
:$\Dom {\bigcup N} = \ds \bigcup_{f \mathop \in N} \Dom f$
where $\Dom f$ denotes the domain of $f$.

Proof:
From Union of Nest of Mappings is Mapping we have that $\bigcup N$ is a mapping.
Let $x \in \Dom {\bigcup N}$.
Then by definition of mapping:
:$\exists \tuple {x, y} \in \bigcup N$
Then by definition of union of class:
:$\exists f \subseteq \bigcup N: \tuple {x, y} \in f$
Hence:
:$\exists f \subseteq \bigcup N: x \in \Dom f$
That is:
:$x \in \ds \bigcup_{f \mathop \in N} \Dom f$
That is:
:$\Dom {\bigcup N} \subseteq \ds \bigcup_{f \mathop \in N} \Dom f$
Let $x \in \ds \bigcup_{f \mathop \in N} \Dom f$.
Then:
:$\exists f \subseteq \bigcup N: x \in \Dom f$
Then by definition of mapping:
:$\exists f \subseteq \bigcup N: \tuple {x, y} \in f$
Thus by definition of union of class:
:$\exists \tuple {x, y} \in \bigcup N$
It follows that:
:$x \in \Dom {\bigcup N}$
That is:
:$\ds \bigcup_{f \mathop \in N} \Dom f \subseteq \Dom {\bigcup N}$
Hence by definition of set equality:
:$\Dom {\bigcup N} = \ds \bigcup_{f \mathop \in N} \Dom f$
{{qed}}
Theorem: Image of Union of Nest of Mappings is Union of Class of Images

Let $N$ be a nest of mappings.
Let $\bigcup N$ denote the union of $N$.
Then:
:$\Img {\bigcup N} = \ds \bigcup_{f \mathop \in N} \Img f$
where $\Img f$ denotes the image of $f$.

Proof:
From Union of Nest of Mappings is Mapping we have that $\bigcup N$ is a mapping.
Let $y \in \Img {\bigcup N}$.
Then by definition of mapping:
:$\exists \tuple {x, y} \in \bigcup N$
Then by definition of union of class:
:$\exists f \subseteq \bigcup N: \tuple {x, y} \in f$
Hence:
:$\exists f \subseteq \bigcup N: y \in \Img f$
That is:
:$y \in \ds \bigcup_{f \mathop \in N} \Img f$
That is:
:$\Img {\bigcup N} \subseteq \ds \bigcup_{f \mathop \in N} \Img f$
Let $y \in \ds \bigcup_{f \mathop \in N} \Img f$.
Then:
:$\exists f \subseteq \bigcup N: y \in \Img f$
Then by definition of mapping:
:$\exists f \subseteq \bigcup N: \tuple {x, y} \in f$
Thus by definition of union of class:
:$\exists \tuple {x, y} \in \bigcup N$
It follows that:
:$y \in \Img {\bigcup N}$
That is:
:$\ds \bigcup_{f \mathop \in N} \Img f \subseteq \Img {\bigcup N}$
Hence by definition of set equality:
:$\Img {\bigcup N} = \ds \bigcup_{f \mathop \in N} \Img f$
{{qed}}
Theorem: Union of Nest of Injections is Injection

Let $N$ be a nest of mappings which are all injections.
Then:
:$\bigcup N$ is an injection
where $\bigcup N$ denotes the union of $N$.

Proof:
From Union of Nest of Mappings is Mapping we have that $\bigcup N$ is a mapping.
{{AimForCont}}:
:$\exists x_1, x_2: \tuple {x_1, y} \in \bigcup N \land \tuple {x_2, y} \in \bigcup N$
such that:
:$x_1 \ne x_2$
Then:
:$\exists f \subseteq \bigcup N: \tuple {x_1, y} \in f$
and:
:$\exists g \subseteq \bigcup N: \tuple {x_1, y} \in g$
But because $N$ is a nest of mappings, either:
:$f \subseteq g$
or:
:$g \subseteq f$
That means either:
:$\tuple {x_1, y} \in g$
or:
:$\tuple {x_2, y} \in f$
Hence either $f$ or $g$ has both $\tuple {x_1, y}$ and $\tuple {x_2, y}$ in it.
That is, either $f$ or $g$ is not an injection.
From this contradiction it follows that if: 
:$\exists x_1, x_2: \tuple {x_1, y} \in \bigcup N \land \tuple {x_2, y} \in \bigcup N$
then it has to be the case that:
:$x_1 = x_2$
It follows that $\bigcup N$ is a an injection.
{{qed}}
Theorem: Well-Ordering on Class is not necessarily Proper

Let $A$ be a class.
Let $\preccurlyeq$ be a well-ordering on $A$.
Then it is not necessarily the case that $\preccurlyeq$ is a proper well-ordering.

Proof:
Proof by Counterexample:
{{ProofWanted}}
Theorem: Order Automorphism on Well-Ordered Class is Forward Moving

Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
Let $\phi$ be an order isomorphism on $\struct {A, \preccurlyeq}$.
Then:
:$\forall a \in A: a \preccurlyeq \map \phi a$

Proof:
Let us define an element $a$ of $A$ such that:
:$\map \phi a \prec a$
as '''moving backwards'''.
{{AimForCont}} there exists an element $a$ of $A$ that '''moves backwards''':
:$\map \phi a \prec a$
for some $a \in A$.
Then applying $\phi$ to both sides:
:$\map \phi {\map \phi a} \prec \map \phi a$
That is:
:$\map \phi a$ also '''moves backwards'''
Thus if some $a \in A$ '''moves backwards''', there is another predecessor element that also '''moves backwards'''.
Hence there is no smallest element of the set of all elements of $A$ that '''move backwards'''.
But this contradicts the properties of a well-ordered class:
:every non-empty subclass of $A$ has a smallest element under $\preccurlyeq$.
Hence there can be no elements of $A$ that '''move backwards'''.
That is:
:$\forall a \in A: a \preccurlyeq \map \phi a$
{{qed}}
Theorem: Order Automorphism on Well-Ordered Class is Identity Mapping

Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
Let $\phi$ be an order isomorphism on $\struct {A, \preccurlyeq}$.
Then $\phi$ is the identity mapping:
:$\forall a \in A: \map \phi a = a$

Proof:
Let $\phi$ be an order isomorphism.
Then from Inverse of Order Isomorphism is Order Isomorphism, the inverse mapping $\phi^{-1}$ is also an order isomorphism.
From Order Automorphism on Well-Ordered Class is Forward Moving:
:$\forall a \in A: a \preccurlyeq \map \phi a$
and:
:$\forall a \in A: a \preccurlyeq \map {\phi^{-1} } a$
from which:
:$\forall a \in A: \map \phi a \preccurlyeq \map \phi {\map {\phi^{-1} } a} = a$
Hence:
:$\forall a \in A: \map \phi a = a$
{{qed}}
Theorem: Well-Ordered Classes are Isomorphic at Most Uniquely

Let $\struct {A, \preccurlyeq_A}$ and $\struct {B, \preccurlyeq_B}$ be well-ordered classes.
Then there exists at most one order isomorphism from $\struct {A, \preccurlyeq_A}$ to $\struct {B, \preccurlyeq_B}$

Proof:
{{questionable|Set-theoretic definitions and proofs are used in the below. They need to be expanded to class-theoretical versions.}}
Let $\phi$ and $\psi$ be order isomorphisms from $A$ to $B$.
Then from Inverse of Order Isomorphism is Order Isomorphism:
:the inverse mapping $\psi^{-1}$ is an order isomorphism from $B$ to $A$.
Hence from Composite of Order Isomorphisms is Order Isomorphism:
:$\phi \circ \psi^{-1}$ is an order isomorphism from $A$ to $A$.
But from Order Automorphism on Well-Ordered Class is Identity Mapping:
:$\phi \circ \psi^{-1}$ is the identity mapping.
From Composite of Mapping with Inverse of Another is Identity implies Mappings are Equal:
:$\phi = \psi$
{{qed}}
Theorem: Well-Ordered Class is not Isomorphic to Initial Segment

Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
There exists no order isomorphism from $\struct {A, \preccurlyeq}$ to an initial segment of $A$.

Proof:
Let $a \in A$.
Let $A_a$ be the initial segment of $A$ determined by $a$.
{{AimForCont}} $\phi: A \to A_a$ is an order isomorphism from $A$ to $A_a$.
From Order Automorphism on Well-Ordered Class is Forward Moving:
:$a \preccurlyeq \map \phi a$
But by definition of initial segment:
:$\map \phi a \notin A_a$
Hence $\phi$ cannot be an order isomorphism.
Hence by Proof by Contradiction there exists no such order isomorphism.
{{qed}}
Theorem: Distinct Ordinals are not Order Isomorphic

Let $\alpha$ and $\beta$ be ordinals such that $\alpha \ne \beta$.
Then $\alpha$ and $\beta$ are not order isomorphic.

Proof:
By definition, an ordinal is well-ordered by the subset relation.
From Class of All Ordinals is Well-Ordered by Subset Relation, the class of all ordinals is a nest.
Hence:
:$\paren {\alpha \subsetneqq \beta} \lor \paren {\beta \subsetneqq \alpha}$
{{finish|there should be a result somewhere that explicitly states that one ordinal is an initial segment of another one}}
The result follows by Well-Ordered Class is not Isomorphic to Initial Segment.
{{qed}}
Theorem: Distinct Lower Sections of Well-Ordered Class are not Order Isomorphic

Let $\struct {A, \preccurlyeq}$ be a well-ordered class.
Let $L_1$ and $L_2$ be distinct lower sections of $\struct {A, \preccurlyeq}$.
Then $L_1$ and $L_2$ are not order isomorphic {{WRT}} $\preccurlyeq$.

Proof:
A lower section of $A$ is a subclass of $A$.
Hence by definition of well-ordered class. $L_1$ and $L_2$ are themselves well-ordered classes.
We have $L_1 \ne L_2$.
The result follows from 
{{finish|Result needed here to the effect that distinct well-ordered classes are not isomorphic. We have this for sets but not classes.}}
Theorem: Isomorphisms between Lower Sections of Well-Ordered Classes are Nested

Let $\struct {A, \preccurlyeq_A}$ and $\struct {B, \preccurlyeq_B}$ be well-ordered classes.
Let $\phi_1$ and $\phi_2$ be order isomorphisms from a lower section of $\struct {A, \preccurlyeq_A}$ to a lower section of $\struct {B, \preccurlyeq_B}$.
Then either:
:$\phi_1 \subseteq \phi_2$
or:
:$\phi_2 \subseteq \phi_1$
where $\subseteq$ denotes the subset relation on mappings:
:$f \subseteq g \iff \forall x \in \Dom f: \map f x = \map g x$

Proof:
Let us label the domains of $\phi_1$ and $\phi_2$:
:$D_1 = \Dom {\phi_1}$
:$D_2 = \Dom {\phi_2}$
Because $D_1$ and $D_2$ are both lower sections of $\struct {A, \preccurlyeq_A}$, they are comparable under the subset relation.
{{WLOG}}, suppose $D_1 \subseteq D_2$.
Then the restriction $\phi_2 {\restriction_{D_1} }$ is an order isomorphisms from $D_1$ to a lower section of $\struct {B, \preccurlyeq_B}$.
From Lower Sections of Well-Ordered Classes are Order Isomorphic at most Uniquely:
:$\phi_2 {\restriction_{D_1} } = \phi_1$
That is:
:$\phi_1 \subseteq \phi_2$
Similarly if $D_2 \subseteq D_1$ then:
:$\phi_2 \subseteq \phi_1$
{{qed}}
Theorem: Sum of Larger Ideals is Larger

Let $R$ be a commutative ring with unity.
Let $\mathfrak a_1, \mathfrak a_2, \mathfrak b_1, \mathfrak b_2$ be ideals of $R$ such that:
:$\mathfrak a_1 \subseteq \mathfrak a_2$
and:
:$\mathfrak b_1 \subseteq \mathfrak b_2$
Then their sums satisfy:
:$\mathfrak a_1 + \mathfrak b_1 \subseteq \mathfrak a_2 + \mathfrak b_2$

Proof:
Let $x \in \mathfrak a_1 + \mathfrak b_1$.
By {{Defof|Sum of Ideals of Ring|Sum of Ideals}}, there are $a \in \mathfrak a_1$ and $a \in \mathfrak b_1$ such that:
:$x = a + b$
Then:
:$a \in \mathfrak a_1 \subseteq \mathfrak a_2$
and:
:$b \in \mathfrak b_1 \subseteq \mathfrak b_2$
Thus, by {{Defof|Sum of Ideals of Ring|Sum of Ideals}}:
:$x \in \mathfrak a_2 + \mathfrak b_2$
{{qed}}
Category:Radical of Ideals
bdtsoj1v3rvjncsilm1g6u1as62sxg3
Theorem: Prime Ideal is Primary Ideal

Let $R$ be a commutative ring with unity.
Let $\mathfrak p$ be a prime ideal of $R$.
Then $\mathfrak p$ is a primary ideal of $R$.

Proof:
Let $xy \in \mathfrak p$.
Let $x \not \in \mathfrak p$
By definition of prime ideal:
:$y^1 = y \in \mathfrak p$
Thus, by definition, $\mathfrak p$ is a primary ideal.
{{qed}}
Category:Prime Ideals of Rings
Category:Primary Ideals
2e1qxhlf2bpm647btf4cvstgy1xgiku
Theorem: Contraction of Primary Ideal is Primary Ideal

Let $A$ and $B$ be commutative rings with unity.
Let $f : A \to B$ be a ring homomorphism.
Let $\mathfrak b$ be a primary ideal of $B$.
Let $\mathfrak b^c$ be the contraction of $\mathfrak b$ by $f$.
Then $\mathfrak b^c$ is a primary ideal of $A$.

Proof:
Let $x,y \in A$ such that:
:$xy \in \mathfrak b^c$.
That is:
:$\map f {xy} = \map f x \map f y \in \mathfrak b$
Suppose that $x \ne \mathfrak b^c$.
That is:
:$\map f x \not \in \mathfrak b$
Since $\mathfrak b$ is primary:
:$\exists n \in \N_{>0} : \map f {y^n} = \paren {\map f y}^n \in \mathfrak b$
That is:
:$y^n \in \mathfrak b^c$
{{qed}}
Category:Primary Ideals
iwe44uqmh607tzewpnes2i1a0pz1hx6
Theorem: Fundamental Property of Norm on Bounded Linear Functional

Let $\Bbb F \in \set {\R, \C}$. 
Let $\struct {X, \norm \cdot_X}$ be a normed vector space over $\Bbb F$.
Let $\struct {X^\ast, \norm \cdot_{X^\ast} }$ be the normed dual of $\struct {X, \norm \cdot_X}$. 
Then for all $x \in X$ and $f \in X^\ast$:
:$\cmod {\map f x} \le \norm f_{X^\ast} \norm x_X$

Proof:
Let $x \in X$ and $f \in X^\ast$.
If $x = 0$, the claim is trivial, since by the linearity of $f$:
:$\cmod {\map f x} = \cmod {\map f 0} = 0$
Let $x \ne 0$.
Recall by {{Defof|Norm/Bounded Linear Functional/Normed Vector Space|Norm of Bounded Linear Functional|index = 3}}:
:$\norm f_{X^\ast} = \sup \set {\dfrac {\cmod {\map f x} } {\norm x_X} : \forall x \in X, x \ne 0}$
Thus, by $\paren 1$ of {{Defof|Supremum of Subset of Real Numbers|Supremum}}:
:$\cmod {\map f x} = \dfrac {\cmod {\map f x} }{\norm x_X} {\norm x_X} \le \norm f_{X^\ast} \norm x_X$
{{qed}}
Category:Bounded Linear Functionals
q1b7zuh9dhyr0qrn9pimo4gno635end
Theorem: Fundamental Theorem of Well-Ordering

Let $\struct {A, \preccurlyeq_A}$ and $\struct {B, \preccurlyeq_B}$ be well-ordered classes.
Then either:
:$\struct {A, \preccurlyeq_A}$ is order isomorphic to a lower section of $\struct {B, \preccurlyeq_B}$, or perhaps all of $\struct {B, \preccurlyeq_B}$
or:
:$\struct {B, \preccurlyeq_B}$ is order isomorphic to a lower section of $\struct {A, \preccurlyeq_A}$, or perhaps all of $\struct {A, \preccurlyeq_A}$.

Proof:
Let $N$ be the class of all order isomorphisms from lower sections of $\struct {A, \preccurlyeq_A}$ which are sets to lower sections of $\struct {B, \preccurlyeq_B}$ which are sets.
Each such order isomorphism is itself a set.
By Isomorphisms between Lower Sections of Well-Ordered Classes are Nested, $N$ is a nest.
$N$ may or may not contain a maximal element {{WRT}} the subset relation.
However, note that no order isomorphism from a proper lower section of $\struct {A, \preccurlyeq_A}$ onto a proper lower section of $\struct {B, \preccurlyeq_B}$ can be a maximal element of $N$.
Indeed, suppose $\psi$ is an order isomorphism from a proper lower section $a^\prec$ of $\struct {A, \preccurlyeq_A}$ onto a proper lower section $b^\prec$ of $\struct {B, \preccurlyeq_B}$.
Then $\psi \cup \tuple {a, b}$ is an element of $N$ which is a proper extension of $\psi$.
Let $I = \bigcup N$ be the union of $N$.
Because $N$ is a nest, $I$ must be an order isomorphism from a lower section of $\struct {A, \preccurlyeq_A}$ (not necessarily proper) onto a lower section of $\struct {B, \preccurlyeq_B}$  (not necessarily proper).
It remains to be shown that either:
:the domain of $I$ is the whole of $A$
or:
:the image of $I$ is the whole of $B$.
Equivalently, we can instead show that:
:the domain of $I$ cannot be a proper lower section of $\struct {A, \preccurlyeq_A}$
and:
:the image of $I$ cannot be a proper lower section of $\struct {B, \preccurlyeq_B}$.
{{AimForCont}}, the above were the case.
Because $I = \bigcup N$, $I$ would then be a maximal element of $N$.
But we have shown that no order isomorphism from a proper lower section of $\struct {A, \preccurlyeq_A}$ onto a proper lower section of $\struct {B, \preccurlyeq_B}$ can be a maximal element of $N$.
Therefore $I$ cannot be an order isomorphism from a proper lower section of $\struct {A, \preccurlyeq_A}$ onto a proper lower section of $\struct {B, \preccurlyeq_B}$.
The result follows.
{{qed}}
Theorem: Axiom of Swelledness is implied by Axiom of Replacement

Let the {{axiom-link|Replacement|Class Theory}} (in the context of class theory) be accepted.
Then the {{axiom-link|Swelledness}} holds.

Proof:
Recall the Axiom of Replacement:
{{:Axiom:Axiom of Replacement/Class Theory/Formulation 1}}
Recall the {{axiom-link|Swelledness}}:
{{:Axiom:Axiom of Swelledness}}
That is:
:Every subclass of a set is a set.
Let $x$ be a set.
Let $A$ be a class such that $A \subseteq x$.
Suppose $A$ is the empty class.
Then by the {{axiom-link|the Empty Set|Class Theory}}, $A$ is a set.
Suppose $A$ is a non-empty class.
Let $c \in A$ be arbitrary.
Let $f$ be:
:the class of all ordered pairs $\tuple {a, a}$ for $a \in A$
along with:
:all ordered pairs $\tuple {y, c}$ where $y \in x \setminus A$.
Thus:
:$f$ is a mapping whose domain is $x$
and:
:$\forall y \in x: \map f y = \begin {cases} y & : y \in A \\ c & : y \notin A \end {cases}$
Thus:
:$\forall y \in x: \map f y \in A$
and in fact:
:$f \sqbrk x = A$
We have {{hypothesis}} that $x$ is a set.
Then by the {{axiom-link|Replacement|Class Theory}}:
:$A$ is therefore also a set.
Hence the result.
{{qed}}
Theorem: Continuous Linear Transformations form Subspace of Linear Transformations

The space of continuous linear transformations is a subspace of the space of linear transformations.

Proof:
Let $\struct {X, \norm \cdot }$ and $\struct {Y, \norm \cdot }$ be normed vector spaces.
Theorem: Axiom of Replacement implies Image of Bijection on Set is Set

Let the Axiom of Replacement (in the context of class theory) be accepted.
Let $A$ be a class which can be put into one-to-one correspondence with a set.
Then $A$ is a set.

Proof:
Let $x$ be a set such that $A$ can be put into one-to-one correspondence with $x$.
Then by definition there exists a bijection from $x$ to $A$.
Let $f: x \to A$ be such a bijection.
Then by the Axiom of Replacement, $f \sqbrk x$ is a set.
But:
:$f \sqbrk x = A$
Hence the result.
{{qed}}
Theorem: Characterization of Convergence in Locally Convex Space

Let $\Bbb F \in \set {\R, \C}$.
Let $\struct {X, \mathcal P}$ be a locally convex space over $\Bbb F$ with standard topology $\tau$.
Let $x \in X$. 
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$. 
Then: 
:$x_n \to x$ in $\struct {X, \tau}$
{{iff}}:
:$\map p {x_n - x} \to 0$ as $n \to \infty$ as a real sequence, for each $p \in \mathcal P$.

Proof:
=== Necessary Condition ===
Suppose that: 
:$x_n \to x$ in $\struct {X, \tau}$
Let $p \in \mathcal P$. 
Let $\epsilon > 0$. 
We aim to show that there exists $N \in \N$ such that: 
:$\map p {x_n - x} < \epsilon$ for $n \ge N$
showing that: 
:$\map p {x_n - x} \to 0$ as $n \to \infty$. 
From the definition of a convergent sequence in a topological space, we have: 
:for each $U \in \tau$ such that $x \in U$, there exists $N \in \N$ such that $x_n \in U$ for $n \ge N$.
From the definition of the standard topology $\tau$, we have: 
:$U = \set {y \in X : \map p {y - x} < \epsilon}$ is open.
So there exists $N \in \N$ such that $x_n \in U$ for $n \ge N$. 
That is: 
:$\map p {x_n - x} < \epsilon$ for $n \ge N$. 
Since $\epsilon$ was arbitrary we have: 
:$\map p {x_n - x} \to 0$ as $n \to \infty$. 
{{qed|lemma}}