avewright/proofwiki-math huggingface dataset:
Theorem: Class under Progressing Mapping such that Elements are Sandwiched is Nest

Let $A$ be a class.
Let $g: A \to A$ be a progressing mapping on $A$ such that:
:$\forall x, y \in A: \map g x \subseteq y \lor y \subseteq x$
Then $A$ is a nest:
:$\forall x, y \in A: x \subseteq y \lor y \subseteq x$

Proof:
By definition of progressing mapping:
:$\forall x \in A: x \subseteq \map g x$
Thus by Subset Relation is Transitive:
:$\map g x \subseteq y \implies x \subseteq y$
and it follows that:
:$\forall x, y \in A: x \subseteq y \lor y \subseteq x$
Hence the result by definition of nest.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then for all $x, y \in M$:

Proof:
From Minimally Inductive Class under Progressing Mapping induces Nest, we have that $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Thus the Sandwich Principle applies directly.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then for all $x, y \in M$:

Proof:
By definition of minimally inductive class, $M$ is minimally closed under $g$ with respect to $\O$.
The result is then seen to be a direct application of Sandwich Principle for Minimally Closed Class.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping/Sandwich Principle

:$x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$

Proof:
From Minimally Inductive Class under Progressing Mapping induces Nest, we have that $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Thus the Sandwich Principle applies directly.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping/Sandwich Principle

:$x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$

Proof:
By definition of minimally inductive class, $M$ is minimally closed under $g$ with respect to $\O$.
The result is then seen to be a direct application of Sandwich Principle for Minimally Closed Class.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping/Image of Proper Subset is Subset

:$x \subset y \implies \map g x \subseteq y$

Proof:
From Minimally Inductive Class under Progressing Mapping induces Nest, we have that $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Thus corollary $1$ of the Sandwich Principle applies directly.
{{qed}}
Theorem: Characteristics of Minimally Inductive Class under Progressing Mapping/Mapping Preserves Subsets

:$x \subseteq y \implies \map g x \subseteq \map g y$

Proof:
From Minimally Inductive Class under Progressing Mapping induces Nest, we have that $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Thus corollary $2$ of the Sandwich Principle applies directly.
{{qed}}
Theorem: Bounded Class is Set

Let $B$ be a class.
Let it be assumed that $B$ is a subclass of a basic universe $V$.
Let $B$ be bounded by a set $x$.
Then $B$ is itself a set.

Proof:
By definition, every element of $B$ is a subset of $x$.
Then every element of $B$ is an element of the power set $\powerset x$ of $x$.
Thus $B$ is a subclass of $\powerset x$.
By the Axiom of Powers, $\powerset x$ is a set.
That is, $\powerset x$ is an element of $V$.
As $V$ is a swelled class, then by definition, then every subclass of $\powerset x$ is an element of $V$.
That includes $B$.
That is, $B$ is an element of $V$.
Thus, by definition of $V$, $B$ is a set.
{{qed}}
Theorem: Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then every non-empty bounded subset of $M$ has a greatest element.

Proof:
Let the hypothesis be assumed.
The proof proceeds by general induction.
For all $x \in M$, let $\map P x$ be the proposition:
:Every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
=== Basis for the Induction ===
Let $x = \O$.
The only non-empty subset of $M$ which is bounded by $\O$ is $\set \O$.
Then it is seen that $\set \O$ has a greatest element, that is $\O$.
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
:Every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
from which it is to be shown that:
:Every non-empty subset of $M$ which is bounded by $\map g x$ has a greatest element.
=== Induction Step ===
This is the induction step:
Let the induction hypothesis be assumed.
Let $B$ be a non-empty subset of $M$ which is bounded by $\map g x$.
Thus, by definition, every element of $B$ is a subset of $\map g x$.
It is to be shown that $B$ has a greatest element $m$.
That is, that $m \in B$ and every element of $B$ is a subset of $m$
Let $\map g x \in B$.
By definition of subset bounded by $\map g x$, every element of $B$ is a subset of $\map g x$.
That is, $\map g x$ is itself the greatest element of $B$.
Suppose that $\map g x \notin B$.
Then every element of $B$ is a proper subset of $\map g x$.
Let $y \in B$ be arbitrary.
Because $y$ is a proper subset of $\map g x$, there exists $z \in \map g x$ such that $z \notin y$.
Thus $\map g x$ is not a subset of $y$.
From Minimally Inductive Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Because it is not the case that $\map g x \subseteq y$, it must be that:
:$y \subseteq x$
Thus, as $y$ is arbitrary, it follows that every element of $B$ is a proper subset of $x$.
Thus $B$ is bounded by $x$.
It follows by the induction hypothesis that $B$ has a greatest element.
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
:For all $x \in M$, every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
That is:
:Every non-empty bounded subset of $M$ has a greatest element.
{{qed}}
Theorem: Projection is Injection iff Factor is Singleton/Family of Sets/Necessary Condition

Let $\family {S_i}_{i \mathop \in I}$ be a non-empty family of non-empty sets where $I$ is an arbitrary index set.
Let $S = \ds \prod_{i \mathop \in I} S_i$ be the Cartesian product of $\family {S_i}_{i \mathop \in I}$.
Let $\pr_j: S \to S_j$ be the $j$th projection on $S$.
Let $\pr_j$ be an injection.
Then $S_i$ is a singleton for all $i \in I \setminus \set j$.

Proof:
Let $\pr_j$ be an injection.
Then:
:$\forall x, y \in S: \map {\pr_j} x = \map {\pr_j} y \implies x = y$
We have that $\family {S_i}_{i \mathop \in I}$ is a non-empty family of non-empty sets
Hence, by the axiom of choice (formulation $2$), $S$ is non-empty.
Let $z \in S$.
By the definition of Cartesian product $S$:
:$\forall i \in I: \map z i \in S_i$.
Let $x_k \in S_k$ for some $k \in I \setminus \set j$.
Let $z' \in S$ be defined by:
:$\map {z'} i = \begin{cases}
\map z i & : i \in I \setminus \set k \\
x_k & : i = k 
\end{cases}$
Then:
{{begin-eqn}}
{{eqn | l = \map {\pr_j} {z'}
      | r = \map {z'} j 
      | c = {{Defof|Projection}}
}}
{{eqn | r = \map z j
      | c = as $j \ne k$ 
}}
{{eqn | r = \map {\pr_j} z
      | c = {{Defof|Projection}}
}}
{{end-eqn}}
Thus:
:$z' = z$
In particular:
:$x_k = \map {z'} k = \map z k = z_k$
It follows that:
:$S_k = \set {z_k}$
Since $k$ was arbitrary:
:$\forall k \in I \setminus \set j: S_k = \set {z_k}$
The result follows.
Theorem: Projection is Injection iff Factor is Singleton/Family of Sets/Sufficient Condition

Let $\family {S_i}_{i \mathop \in I}$ be a non-empty family of non-empty sets where $I$ is an arbitrary index set.
Let $S = \ds \prod_{i \mathop \in I} S_i$ be the Cartesian product of $\family {S_i}_{i \mathop \in I}$.
Let $\pr_j: S \to S_j$ be the $j$th projection on $S$.
Let $S_i$ be a singleton for all $i \in I \setminus \set j$.
Then $\pr_j$ is an injection.

Proof:
Let $S_i = \set {s_i}$ for all $i \in I \setminus \set {j}$.
Let $\map {\pr_j} x = \map {\pr_j} y = s_j$ for $x, y \in S$.
By definition of $j$th projection:
:$\map x j = \map {\pr_j} x = s_j$
:$\map y j = \map {\pr_j} y = s_j$
and so $\map x j = \map y j$.
By the definition of Cartesian product, for all $i \in I \setminus \set j$:
:$\map x i, \map y i \in S_i = \set {s_i}$
and so $\map x i = \map y i$ for all $i \in I \setminus \set j$.
Thus $x = y$.
Thus $\pr_j$ is an injection by definition.
Theorem: Product Space of Subspaces is Subspace of Product Space

Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds T = \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
Let $\family {\struct {Y_i, \upsilon_i} }_{i \mathop \in I}$ be a family of topological spaces such that:
:$\forall i \in I: \struct {Y_i, \upsilon_i}$ is a topological subspace of $\struct {X_i, \tau_i}$
Let $\ds S = \struct {Y, \upsilon} = \prod_{i \mathop \in I} \struct {Y_i, \upsilon_i}$ be the product space of $\family {\struct {Y_i, \upsilon_i} }_{i \mathop \in I}$.
Let $T_Y = \struct {Y, \tau_Y}$ be the topological subspace of $T$.
Then $S = T_Y$.

Proof:
From Cartesian Product of Family of Subsets, $Y \subseteq X$.
Thus the topological subspace $T_Y$ is well-defined.
From Natural Basis of Product Topology, a (synthetic) basis for $T$ is:
:$\ds \BB_T = \set {\prod_{i \mathop \in I} U_i : U_i \in \tau_i, U_i = X_i \text{ for all but finitely many } i \in I}$
From Basis for Topological Subspace a (synthetic) basis for $T_Y$ is:
:$\BB_Y = \set {U \cap Y: U \in \BB_T}$
That is:
{{begin-eqn}}
{{eqn | l = \BB_Y
      | r = \set {\paren {\prod_{i \mathop \in I} U_i} \bigcap \paren {\prod_{i \mathop \in I} Y_i}: U_i \in \tau_i, U_i = X_i \text{ for all but finitely many } i \in I}
}}
{{eqn | r = \set {\prod_{i \mathop \in I} \paren {U_i \cap Y_i}: U_i \in \tau_i, U_i = X_i \text{ for all but finitely many } i \in I}
      | c = General Case of Cartesian Product of Intersections
}}
{{end-eqn}}
By definition of a subspace topology,
:$\forall i \in I: \upsilon_i = \set{U \cap S_i: U \in \tau_i}$
From Natural Basis of Product Topology a (synthetic) basis for $S$ is:
:$\ds \BB_S = \set {\prod_{i \mathop \in I} V_i: V_i \in \upsilon_i, V_i = Y_i \text{ for all but finitely many } i \in I}$
That is:
{{begin-eqn}}
{{eqn | l = \BB_S
      | r = \set {\prod_{i \mathop \in I} \paren{U_i \cap Y_i}: U_i \in \tau_i, U_i \cap Y_i = Y_i \text{ for all but finitely many } i \in I}
}}
{{eqn | r = \set {\prod_{i \mathop \in I} \paren{U_i \cap Y_i}: U_i \in \tau_i, U_i = X_i \text{ for all but finitely many } i \in I}
      | c = as $Y_i \subseteq X_i$ for all $i \in I$
}}
{{end-eqn}}
Thus $\BB_S = \BB_Y$ and therefore $S = T_Y$.
{{qed}}
Category:Product Topology
Category:Subsets
5q2nvr7xa950ppq4dy4n0pzotjq6zaz
Theorem: Difference of Complex Conjugates

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ denote the complex conjugate of the complex number $z$.
Then:
:$\overline {z_1 - z_2} = \overline {z_1} - \overline {z_2}$

Proof:
Let $w = -z_2$.
Then:
{{begin-eqn}}
{{eqn | l = \overline {z_1 - z_2}
      | r = \overline {z_1 + \paren {-z_2} }
      | c = {{Defof|Complex Subtraction}}
}}
{{eqn | r = \overline {z_1 + w}
      | c = Definition of $w$
}}
{{eqn | r = \overline {z_1} + \overline w
      | c = Sum of Complex Conjugates
}}
{{eqn | r = \overline {z_1} + \overline {-z_2}
      | c = Definition of $w$
}}
{{eqn | r = \overline {z_1} - \overline {z_2}
      | c = {{Defof|Complex Subtraction}}
}}
{{end-eqn}}
{{qed}}
Theorem: Nonzero Natural Number is Successor

Let $\N$ be the $0$-based natural numbers:
:$\N = \set {0, 1, 2, \ldots}$
Let $s: \N \to \N: \map s n = n + 1$ be the successor mapping.
Then:
:$\forall n \in \N \setminus \set 0 \paren {\exists m \in \N: \map s m = n}$

Proof:
The proof will proceed by the Principle of Finite Induction on $\N \setminus \set 0$.
Theorem: Determinant with Columns Transposed

If two columns of a matrix with determinant $D$ are transposed, its determinant becomes $-D$.

Proof:
Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
Let $\map \det {\mathbf A}$ be the determinant of $\mathbf A$.
Let $1 \le r < s \le n$.
Let $\mathbf B$ be $\mathbf A$ with columns $r$ and $s$ transposed.
Consider:
:the transpose $\mathbf A^\intercal$ of $\mathbf A$
:the transpose $\mathbf B^\intercal$ of $\mathbf B$.
hence $\mathbf B^\intercal$ is $\mathbf A^\intercal$ with rows $r$ and $s$ transposed.
From Determinant with Rows Transposed:
:$\map \det {\mathbf B^\intercal} = -\map \det {\mathbf A^\intercal}$
From from Determinant of Transpose:
:$\map \det {\mathbf B^\intercal} = \map \det {\mathbf B}$
:$\map \det {\mathbf A^\intercal} = \map \det {\mathbf A}$
and the result follows.
{{qed}}
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 1/Lemma 2

:$\pr_i {\restriction_{Y_i} } = p_i$

Proof:
For all $y \in Y_i$:
{{begin-eqn}}
{{eqn | l = \map {\pr_i {\restriction_{Y_i} } } y
      | r = \map {\pr_i} y
      | c = {{Defof|Restriction of Mapping}}: $\pr_i {\restriction_{Y_i} } : Y_i \to X_i$
}}
{{eqn | r = y_i
      | c = {{Defof|Projection}}: $\pr_i: X \to X_i$
}}
{{eqn | r = \map {p_i} y
      | c = {{Defof|Projection}}: $p_i: Y_i \to X_i$
}}
{{end-eqn}}
By Equality of Mappings:
:$\pr_i {\restriction_{Y_i} } = p_i$
{{qed}}
Category:Subspace of Product Space is Homeomorphic to Factor Space
bl3c2isqpkjid8xkeik842pk548084g
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Proof 1/Lemma 1

:$Y_i = \prod_{j \mathop \in I} Z_j$

Proof:
{{begin-eqn}}
{{eqn | r = x \in Y_i
      | o =
}}
{{eqn | ll = \leadstoandfrom
      | q = \forall j \in I
      | l = x_j
      | r = \begin {cases} z_j & j \ne i \\ x_i \in X_i & i = j \end {cases}
      | c = Definition of $Y_i$
}}
{{eqn | ll = \leadstoandfrom
      | q = \forall j \in I
      | l = x_j
      | o = \in
      | r =  Z_j
      | c = Definition of $Z_j$ for all $j \in I$
}}
{{eqn | ll = \leadstoandfrom
      | l = x
      | o = \in
      | r = \prod_{j \mathop \in I} Z_j
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
The result follows by definition of set equality.
{{qed}}
Category:Subspace of Product Space is Homeomorphic to Factor Space
nxrajfn1e4sq5typfm756zoz792hljp
Theorem: Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x$ be a fixed point of $g$.
Then $x$ is the greatest element of $M$.

Proof:
Let $x$ be an element of $M$ such that $\map g x = x$.
From Empty Set is Subset of All Sets, we have that:
:$\O \subseteq x$
Suppose that $y \subseteq x$.
Then by Characteristics of Minimally Inductive Class under Progressing Mapping:
:$\map g y \subseteq \map g x$
But we have that $\map g x = x$.
Thus:
:$\map g y \subseteq x$
That is:
:$\O \subseteq x$
and:
:$y \subseteq x \implies \map g y \subseteq x$
and the result follows by the Principle of General Induction.
{{qed}}
Theorem: Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x$ be a fixed point of $g$.
Then $x$ is the greatest element of $M$.

Proof:
A minimally inductive class under $g$ is the same thing as a minimally closed class under $g$ with respect to $\O$.
The result then follows by a direct application of Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element.
{{qed}}
Theorem: Closed Class under Progressing Mapping Lemma

Let $N$ be a class which is closed under a progressing mapping $g$.
Let $g$ be such that:
:$\forall x, y \in N: \map g x \subseteq y \lor y \subseteq x$
:if $\map g x = x$, then $x$ is the greatest element of $N$.
Let the following hold:
:$A \subseteq N$ is a subclass of $N$
:$x \in N$ is an element of $N$
Let $x$ be:
:a proper subset of all elements of $A$
and:
:the greatest element of $A$ with that property.
Then $\map g x \in A$ and is the smallest element of $A$.

Proof:
Let the hypothesis be assumed.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
Let $x$ be the greatest element of $L$.
It is to be shown that $\map g x$ is the smallest element of $A$.
We have that $x$ is a proper subset of all elements of $A$.
Then by {{Corollary|Sandwich Principle|1}}:
:$\map g x$ is a subset of all elements of $A$.
It remains to be shown that $\map g x$ is itself an element of $A$.
We have that $x$ is a proper subset of all elements of $A$.
We also have that $x$ contains at least one element.
Therefore $x$ cannot be the greatest element of $N$.
Therefore, {{hypothesis}}:
:$x \ne \map g x$
Thus $x$ is a proper subset of $\map g x$.
Because $x$ is the greatest element of $L$, $\map g x$ is not therefore an element of $L$.
Therefore there exists at least $1$ element $y$ of $A$ such that $\map g x$ is not a proper subset of $y$.
But we have shown that $\map g x \subseteq y$.
Hence:
:$\map g x = y$
and so:
:$\map g x \in A$
Hence the result.
{{qed}}
Theorem: Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x$ be a fixed point of $g$.
Then $M$ is well-ordered under the subset relation.

Proof:
According to hypothesis, let $M$ be minimally inductive under $g$.
By Minimally Inductive Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
By Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element:
:if $x$ is a fixed point of $g$, then $x$ is the greatest element of $M$.
Thus the conditions for Closed Class under Progressing Mapping Lemma hold.
In order to show that $M$ is well-ordered under the subset relation, it is to be shown that every non-empty subclass $A$ of $M$ has a smallest element.
Let $A$ be an arbitrary non-empty subclass of $N$.
Let $L$ be the class of all elements $y$ of $N$ such that $y$ is a proper subset of all elements of $A$.
If $\O \in A$, then $\O$ is the smallest element of $A$.
So, consider the case where $\O \notin A$.
Then $\O$ is a proper subset of every element of $A$.
Thus $\O \in L$ and so $L$ is non-empty.
By definition, $L$ is bounded by all elements of $A$.
Since $A$ is non-empty, $L$ is bounded by at least one element of $A$.
Hence by Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element:
:$L$ has a greatest element $x$.
Therefore, by Closed Class under Progressing Mapping Lemma, $\map g x$ is the smallest element of $A$.
{{qed}}
Theorem: Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x$ be a fixed point of $g$.
Then $M$ is well-ordered under the subset relation.

Proof:
A minimally inductive class under $g$ is the same thing as a minimally closed class under $g$ with respect to $\O$.
The result then follows by a direct application of Minimally Closed Class under Progressing Mapping is Well-Ordered.
{{qed}}
Theorem: Minimally Closed Class under Progressing Mapping induces Nest

For all $x, y \in N$:
:either $\map g x \subseteq y$ or $y \subseteq x$
and $N$ forms a nest:
:$\forall x, y \in N: x \subseteq y$ or $y \subseteq x$

Proof:
Let $\RR$ be the relation on $N$ defined as:
:$\forall x, y \in N: \map \RR {x, y} \iff \map g x \subseteq y \lor y \subseteq x$
We are given that $g$ is a progressing mapping.
From the Progressing Function Lemma, we have that:
{{begin-axiom}}
{{axiom | n = 1
        | q = \forall y \in \Dom g
        | ml= \map \RR {y, \O}
}}
{{axiom | n = 2
        | q = \forall x, y \in \Dom g
        | ml= \map \RR {x, y} \land \map \RR {y, x}
        | mo= \implies
        | mr= \map \RR {x, \map g y}
}}
{{end-axiom}}
In what follows, $(1)$ is not needed.
From the Double Induction Principle for Minimally Closed Class, if $\RR$ is a relation on $N$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in N
        | m = \map \RR {x, b}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in N
        | m = \map \RR {x, y} \land \map \RR {y, x} \implies \map \RR {x, \map g y}
}}
{{end-axiom}}
then $\map \RR {x, y}$ holds for all $x, y \in N$.
As $\Dom g = N$ it is seen that $(\text D 2)$ is fulfilled by $(2)$ directly.
It remains to be demonstrated that $(\text D 1)$ holds.
Indeed, from Smallest Element of Minimally Closed Class under Progressing Mapping, we have that:
:$\forall x \in N: b \subseteq x$
By the Rule of Addition:
:$\forall x \in N: \map g x \subseteq b \lor b \subseteq x$
That is:
:$\forall x \in N: \map \RR {x, b}$
Thus by the Double Induction Principle for Minimally Closed Class:
:$\forall x, y \in N: \map \RR {x, y}$
That is:
:$\forall x, y \in N: \map g x \subseteq y \lor y \subseteq x$
{{qed|lemma}}
As $g$ is a progressing mapping, we have:
:$x \subseteq \map g x$
Hence from:
:$\map g x \subseteq y \lor y \subseteq x$
we have:
:$x \subseteq y \lor y \subseteq x$
Hence the result by definition of a nest.
{{qed}}
Theorem: Minimally Closed Class under Progressing Mapping

Statement of Conditions:
{{:Minimally Closed Class under Progressing Mapping/Statement}}
Then the following results hold:
=== Minimally Closed Class under Progressing Mapping induces Nest ===
{{:Minimally Closed Class under Progressing Mapping induces Nest}}
=== Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element ===
{{:Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element}}
=== Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element ===
{{:Fixed Point of Progressing Mapping on Minimally Closed Class is Greatest Element}}
=== Minimally Closed Class under Progressing Mapping is Well-Ordered ===
{{:Minimally Closed Class under Progressing Mapping is Well-Ordered}}
=== Smallest Element of Minimally Closed Class under Progressing Mapping ===
{{:Smallest Element of Minimally Closed Class under Progressing Mapping}}

Proof:
Let $\RR$ be the relation on $N$ defined as:
:$\forall x, y \in N: \map \RR {x, y} \iff \map g x \subseteq y \lor y \subseteq x$
We are given that $g$ is a progressing mapping.
From the Progressing Function Lemma, we have that:
{{begin-axiom}}
{{axiom | n = 1
        | q = \forall y \in \Dom g
        | ml= \map \RR {y, \O}
}}
{{axiom | n = 2
        | q = \forall x, y \in \Dom g
        | ml= \map \RR {x, y} \land \map \RR {y, x}
        | mo= \implies
        | mr= \map \RR {x, \map g y}
}}
{{end-axiom}}
In what follows, $(1)$ is not needed.
From the Double Induction Principle for Minimally Closed Class, if $\RR$ is a relation on $N$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in N
        | m = \map \RR {x, b}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in N
        | m = \map \RR {x, y} \land \map \RR {y, x} \implies \map \RR {x, \map g y}
}}
{{end-axiom}}
then $\map \RR {x, y}$ holds for all $x, y \in N$.
As $\Dom g = N$ it is seen that $(\text D 2)$ is fulfilled by $(2)$ directly.
It remains to be demonstrated that $(\text D 1)$ holds.
Indeed, from Smallest Element of Minimally Closed Class under Progressing Mapping, we have that:
:$\forall x \in N: b \subseteq x$
By the Rule of Addition:
:$\forall x \in N: \map g x \subseteq b \lor b \subseteq x$
That is:
:$\forall x \in N: \map \RR {x, b}$
Thus by the Double Induction Principle for Minimally Closed Class:
:$\forall x, y \in N: \map \RR {x, y}$
That is:
:$\forall x, y \in N: \map g x \subseteq y \lor y \subseteq x$
{{qed|lemma}}
As $g$ is a progressing mapping, we have:
:$x \subseteq \map g x$
Hence from:
:$\map g x \subseteq y \lor y \subseteq x$
we have:
:$x \subseteq y \lor y \subseteq x$
Hence the result by definition of a nest.
{{qed}}