avewright/proofwiki-math huggingface dataset:
Theorem: Natural Number is not Subset of its Union

Let $n \in \N$ be a natural number as defined by the von Neumann construction.
Then, except in the degenerate case where $n = 0$, it is not the case that:
:$n \subseteq \bigcup n$

Proof:
First we note that from Union of Empty Set we have:
:$\bigcup \O = \O$
leading to:
:$\O \subseteq \bigcup \O$
thus disposing of the degenerate case.
Let $n \in \N$ such that $n \ne \O$.
By definition of the von Neumann construction:
:$n = \set {0, 1, 2, \ldots, n - 1}$
Thus, by definition, $m \in n$ for $m = 0, 1, 2, \ldots, n - 1$.
From Natural Numbers cannot be Elements of Each Other, it cannot therefore be the case that $n \in m$ for $m \in n$.
By definition of union of class:
:$\bigcup n = \set {x: \exists X \in n: x \in X}$
But it has been established that there is no $X \in n$ such that $n \in X$.
Hence the result.
{{qed}}
Theorem: Natural Number is Superset of its Union

Let $n \in \N$ be a natural number as defined by the von Neumann construction.
Then:
:$\bigcup n \subseteq n$

Proof:
Let $n \in \N$.
From Natural Number is Transitive Set, $n$ is transitive.
From Class is Transitive iff Union is Subclass it follows directly that:
:$\bigcup n \subseteq n$
{{qed}}
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Product with Singleton

Let $T_1$ and $T_2$ be non-empty topological spaces.
Let $b \in T_2$.
Let $T_1 \times T_2$ be the product space of $T_1$ and $T_2$.
Let $T_2 \times T_1$ be the product space of $T_2$ and $T_1$.
Then:
:$T_1$ is homeomorphic to the subspace $T_1 \times \set b$ of $T_1 \times T_2$
:$T_1$ is homeomorphic to the subspace $\set b \times T_1$ of $T_2 \times T_1$

Proof:
From Finite Cartesian Product of Non-Empty Sets is Non-Empty both $T_1 \times T_2$ and $T_2 \times T_1$ are both non-empty.
The conclusions follow immediately from Subspace of Product Space is Homeomorphic to Factor Space.
{{qed}}
Theorem: Subspace of Product Space is Homeomorphic to Factor Space/Product with Singleton

Let $T_1$ and $T_2$ be non-empty topological spaces.
Let $b \in T_2$.
Let $T_1 \times T_2$ be the product space of $T_1$ and $T_2$.
Let $T_2 \times T_1$ be the product space of $T_2$ and $T_1$.
Then:
:$T_1$ is homeomorphic to the subspace $T_1 \times \set b$ of $T_1 \times T_2$
:$T_1$ is homeomorphic to the subspace $\set b \times T_1$ of $T_2 \times T_1$

Proof:
The conclusions are symmetrical.
{{WLOG}}, therefore, it will be shown that $T_1$ is homeomorphic to the subspace $T_1 \times \set b$ of $T_1 \times T_2$.
Let $f: T_1 \to T_1 \times \set b$ be defined as:
:$\map f x = \tuple {x, b}$
=== Lemma ===
{{:Subspace of Product Space is Homeomorphic to Factor Space/Product with Singleton/Lemma}}{{qed|lemma}}
$f^{-1}$ is a restriction to the subspace $T_1 \times \set b$ of the projection $\pr_1$ of $T_1 \times T_2$ onto $T_1$.
From Projection from Product Topology is Continuous , $\pr_1$ is a continuous.
From Restriction of Continuous Mapping is Continuous, $f^{-1}$ is a continuous.
It is to be shown that $f$ is continuous.
Let $x \in T_1$.
Let $U$ be an open set in $T_1 \times \set b$ such that:
:$\map f x \in U$
By definition of the subspace topology then for some $U'$ open in $T_1 \times T_2$:
:$U' \cap \paren {T_1 \times \set b} = U$
By the definition of the Natural Basis of Product Topology, there exist open sets $V_1$ and $V_2$ in $T_1$ and $T_2$, respectively, such that:
:$\map f x = \tuple {x, b} \in V_1 \times V_2 \subseteq U'$
Then for any $y \in V_1$:
:$\map f y = \tuple {y, b} \in V_1 \times V_2 \subseteq U'$
But:
:$\tuple {y, b} \in T_1 \times \set b$
so:
:$\tuple {y, b} \in U$
Thus if $y \in V_1$, it follows that $\map f y \in U$.
Then $f$ is continuous by definition.
{{qed}}
Theorem: Natural Number is Union of its Successor

Let $n \in \N$ be a natural number as defined by the von Neumann construction.
Then:
:$\map \bigcup {n^+} = n$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \map \bigcup {n^+}
      | c = 
}}
{{eqn | r = \map \bigcup {\set n \cup n}
      | c = {{Defof|Von Neumann Construction of Natural Numbers}}
}}
{{eqn | r = \bigcup \set n \cup \bigcup n
      | c = Set Union is Self-Distributive
}}
{{eqn | r = n \cup \bigcup n
      | c = Union of Singleton
}}
{{end-eqn}}
From Natural Number is Superset of its Union we have:
:$\bigcup n \subseteq n$
Then from Union with Superset is Superset:
:$\bigcup n \subseteq n \iff \paren {n \cup \bigcup n} = n$
and the result follows.
{{qed}}
Theorem: Set of Natural Numbers Equals its Union

Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction on a Zermelo universe $V$.
Then:
:$\bigcup \omega = \omega$

Proof:
We have {{hypothesis}} that:
:$\omega \in V$
where $V$ is a Zermelo universe.
By the {{axiom-link|Infinity|Class Theory}} we have that $\omega$ is a set.
By the {{axiom-link|Transitivity}}, $\omega$ is transitive.
Hence by Class is Transitive iff Union is Subclass:
:$\bigcup \omega \subseteq \omega$
{{qed|lemma}}
Let $n \in \omega$.
Then by definition of the von Neumann construction:
:$n + 1 = n \cup \set n$
That is:
:$\exists X \in \omega: n \in X$
where in this case $X = n + 1$.
Thus we have that:
:$n \in \set {x: \exists X \in \omega: x \in X}$
and so by definition of union of class:
:$n \in \bigcup \omega$
Thus we have that:
:$\omega \subseteq \bigcup \omega$
which, together with:
:$\bigcup \omega \subseteq \omega$
gives us, by set equality:
:$\bigcup \omega = \omega$
{{qed}}
Theorem: Set of Natural Numbers Equals Union of its Successor

Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction on a Zermelo universe $V$.
Then:
:$\bigcup \omega^+ = \omega$

Proof:
We have that:
:$\omega^+ = \omega \cup \set \omega$
and so:
:$\omega \subseteq \omega^+$
{{qed|lemma}}
By definition:
:$\bigcup \omega^+ = \set {x: \exists y \in \omega^+: x \in y}$
Thus:
:$x \in \bigcup \omega^+ \implies x \in \omega$
{{qed|lemma}}
So by definition of set equality:
:$\bigcup \omega^+ = \omega$
{{qed}}
Theorem: Equivalence of Definitions of Minimally Inductive Class

Let $A$ be a class.
Let $g$ be a mapping on $A$.
{{TFAE|def = Minimally Inductive Class under General Mapping|view = minimally inductive class under $g$}}

Proof:
=== $(1)$ implies $(2)$ ===
Let it be given that $A$ is inductive under $g$.
Let $A$ be a minimally inductive class under $g$ by definition 1.
Then by definition:
:$A$ has no proper subclass $B$ such that $B$ is inductive under $g$.
Let $A$ have a subclass $C$ which is inductive under $g$.
Then by definition, $C$ is not a proper subclass of $A$.
Thus by definition of proper subclass:
:$C = A$
By definition of subclass:
:$A \subseteq C$
and:
:$C \subseteq A$
That is:
:$\forall x \in A: x \in C$
and:
:$\forall x \in C: x \in A$
That is:
$C$ contains all elements of $A$.
Thus $A$ is a minimally inductive class under $g$ by definition 2.
{{qed|lemma}}
Theorem: Principle of General Induction

Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be minimally inductive under $g$.
Let $P: M \to \set {\T, \F}$ be a propositional function on $M$.
Suppose that:
{{begin-axiom}}
{{axiom | n = 1
        | ml= \map P \O
        | mo= =
        | mr= \T
}}
{{axiom | n = 2
        | q = \forall x \in M
        | ml= \map P x
        | mo= =
        | mr= \T \implies \map P {\map g x} = \T
}}
{{end-axiom}}
Then:
:$\forall x \in M: \map P x = \T$

Proof:
We are given that $M$ is a minimally inductive class under $g$.
That is, $M$ is an inductive class under $g$ with the extra property that $M$ has no proper class which is also an inductive class under $g$.
Let $P$ be a propositional function on $M$ which has the properties specified:
:$(1): \quad \map P \O = \T$
:$(2): \quad \forall x \in M: \map P x = \T \implies \map P {\map g x} = \T$
Thus by definition, the class $S$ of all elements of $M$ such that $\map P x = \T$ is an inductive class under $g$.
But because $M$ is minimally inductive under $g$, $S$ contains all elements of $M$.
That is:
:$\forall x \in M: \map P x = \T$
as we were to show.
{{Qed}}
Theorem: Von Neumann Construction of Natural Numbers is Minimally Inductive

Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction.
$\omega$ is a minimally inductive class under the successor mapping.

Proof:
Consider Peano's axioms:
{{:Axiom:Peano's Axioms}}
From Inductive Construction of Natural Numbers fulfils Peano's Axioms, $\omega$ fulfils Peano's axioms.
We note that from {{PeanoAxiom|1}}:
:$\O \in \omega$
We acknowledge from {{PeanoAxiom|2}}:
:the successor mapping defines that $n^+ := n \cup \set n$
and from {{PeanoAxiom|5}} the result follows.
{{qed}}
Theorem: Cartesian Product of Subsets/Family of Subsets

Let $\family {S_i}_{i \mathop \in I}$ be a family of 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 $\family {T_i}_{i \mathop \in I}$ be a family of sets.
Let $T = \ds \prod_{i \mathop \in I} T_i$ be the Cartesian product of $\family {T_i}_{i \mathop \in I}$.
Then:
:$\paren {\forall i \in I: T_i \subseteq S_i} \implies T \subseteq S$.

Proof:
Let $T_i \subseteq S_i$ for all $i \in I$.
Then:
{{begin-eqn}}
{{eqn | l = \family {x_i}
      | o = \in
      | r = T
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall i \in I
      | l = x_i
      | o = \in
      | r = T_i
      | c = {{Defof|Cartesian Product of Family}}
}}
{{eqn | ll= \leadsto
      | q = \forall i \in I
      | l = x_i
      | o = \in
      | r = S_i
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = \family {x_i}
      | o = \in
      | r = S
      | c = {{Defof|Cartesian Product of Family}}
}}
{{end-eqn}}
Thus $T \subseteq S$ by the definition of a subset.
{{qed}}
Category:Cartesian Product of Subsets
Category:Indexed Families
rfced7ro0r4com9nnlgzjyztu4pwi5p
Theorem: Double Induction Principle

Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Let $\RR$ be a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, \O}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | 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 M$.

Proof:
The proof proceeds by general induction.
Let an element $x$ of $M$ be defined as:
:'''left normal''' with respect to $\RR$ {{iff}} $\map \RR {x, y}$ for all $y \in M$
:'''right normal''' with respect to $\RR$ {{iff}} $\map \RR {y, x}$ for all $y \in M$.
Let the hypothesis be assumed.
First we demonstrate a lemma:
=== Lemma ===
{{:Double Induction Principle/Lemma}}{{qed|lemma}}
We now show by general induction that every $x \in M$ is right normal with respect to $\RR$.
It then follows from the lemma that $\map \RR {x, y}$ for all $x, y \in M$.
=== Basis for the Induction ===
$\map P \O$ is the case:
From condition $\text D_1$ of the definition of $\RR$, we have immediately that:
:$\map \RR {x, \O}$
for all $x \in M$.
That is, that $\O$ is right normal with respect to $\RR$.
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:
:$x$ is right normal with respect to $\RR$
from which it is to be shown that:
:$\map g x$ is right normal with respect to $\RR$.
=== Induction Step ===
This is the induction step:
Let $x \in M$ be right normal with respect to $\RR$:
:$\forall y \in M: \map \RR {y, x}$
By the lemma we have that $x$ is left normal with respect to $\RR$.
That is:
:$\forall y \in M: \map \RR {x, y}$
Thus by condition $\text D_2$ of the definition of $\RR$:
:$\forall y \in M: \map \RR {y, \map g x}$
That is, $\map g x$ is right normal with respect to $\RR$.
So $\map P x \implies \map P {\map g x}$ and by the Principle of General Induction:
:$\forall x \in M$: $x$ is right normal with respect to $\RR$.
The result follows.
{{qed}}
Theorem: Double Induction Principle

Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Let $\RR$ be a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, \O}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | 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 M$.

Proof:
By definition, a minimally inductive class under $g$ is a minimally closed class under $g$ with respect to $\O$.
Recall the Double Induction Principle for Minimally Closed Class:
Let $\RR$ be a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, b}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | 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 M$.
In this context:
:$b = \O$
and the result follows.
{{qed}}
Theorem: Successor Mapping on Natural Numbers is Progressing

Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction.
Let $s: \omega \to \omega$ denote the successor mapping on $\omega$.
Then $s$ is a progressing mapping.

Proof:
By definition of the von Neumann construction:
:$n^+ = n \cup \set n$
from which it follows that:
:$n \subseteq n^+$
Hence the result by definition of progressing mapping.
{{qed}}
Theorem: Successor Mapping on Natural Numbers is Progressing

Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction.
Let $s: \omega \to \omega$ denote the successor mapping on $\omega$.
Then $s$ is a progressing mapping.

Proof:
By definition, the successor mapping on $\omega$ is indeed an example of a successor mapping.
The result follows from Successor Mapping is Progressing.
{{qed}}
Theorem: Cartesian Product of Subsets/Family of Nonempty Subsets

Let $T_i \ne \O$ for all $i \in I$.
Then:
:$T \subseteq S \iff \forall i \in I: T_i \subseteq S_i$.

Proof:
From Cartesian Product of Family of Subsets:
:$\paren {\forall i \in I: T_i \subseteq S_i} \implies T \subseteq S$
So it remains to show that:
:$T \subseteq S \implies \forall i \in I : T_i \subseteq S_i$.
Let $T \subseteq S$.
Let $x_j \in T_j$ for some $j \in I$.
Let $\map x j = x_j$
Suppose $k \in I: k \ne j$.
As $T_k \ne \O$ it is possible to use the axiom of choice to choose $\map x k \in T_k$.
Then:
:$x \in T \subseteq S$
By definition of the Cartesian product $S$:
:$\forall i \in I: \map x i \in S_i$
In particular:
:$\map x j = x_j \in S_j$
As $x_j$ is an arbitrary element of $T_j$:
:$T_j \subseteq S_j$
As $j$ is an arbitrary element of $I$:
:$\forall i \in I: T_i \subseteq S_i$
The result follows. 
{{qed}}
{{AoC}}
Category:Cartesian Product of Subsets
Category:Indexed Families
65mn7a0dpake6ha68jmd075n1kabwho
Theorem: Projection is Injection iff Factor is Singleton/Family of Sets

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$.
Then $\pr_j$ is an injection {{iff}} $S_i$ is a singleton for all $i \in I \setminus \set j$.

Proof:
=== Sufficient Condition ===
{{:Projection is Injection iff Factor is Singleton/Family of Sets/Sufficient Condition}}{{qed|lemma}}
Theorem: Progressing Function Lemma

Let $A$ be a class.
Let $g$ be a progressing mapping on $A$.
Let $\RR$ be the relation defined as:
:$\map \RR {x, y} \iff \map g x \subseteq y \lor y \subseteq x$
where $\lor$ denotes disjunction (inclusive "or").
Then:
{{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}}
where $\land$ denotes conjunction ("and").

Proof:
In the following, let $x$ and $y$ be arbitrary elements of $A$ in the domain of $g$.
From Empty Set is Subset of All Sets:
:$\O \subseteq y$
Thus by the Rule of Addition:
:$\map g y \subseteq \O \lor \O \subseteq y$
and so it is seen that $\map \RR {y, \O}$.
That is, $(1)$ holds.
{{qed|lemma}}
Let $\map \RR {x, y}$ and $\map \RR {y, x}$ both hold.
Thus by definition of $\RR$, both of the following hold:
:$(\text a): \quad \map g x \subseteq y$ or $y \subseteq x$
:$(\text b): \quad \map g y \subseteq x$ or $x \subseteq y$
We are to show that $\map \RR {x, \map g y}$ holds.
That is:
:$\map g x \subseteq \map g y$ or $\map g y \subseteq x$
Let $\map g x \subseteq y$.
Because $g$ is a progressing mapping:
:$y \subseteq \map g y$
and so:
:$\map g x \subseteq \map g y$
Thus $\map \RR {x, \map g y}$ holds.
{{qed|lemma}}
Let $\map g y \subseteq x$.
Then by definition $\map \RR {x, \map g y}$ holds.
{{qed|lemma}}
If neither $\map g x \subseteq y$ nor $\map g y \subseteq x$, then by $(\text a)$ and $(\text b)$:
:$y \subseteq x$ and $x \subseteq y$
and so by definition of set equality:
:$x = y$
Hence:
:$\map g x = \map g y$
Thus, again by definition of set equality:
:$\map g x \subseteq \map g y$
and so again, by definition, $\map \RR {x, \map g y}$ holds.
{{qed|lemma}}
Thus it has been shown that in all cases, if $\map \RR {x, y}$ and $\map \RR {y, x}$ both hold, then $\map \RR {x, \map g y}$ holds.
Thus condition $(2)$ has been satisfied.
Hence the result.
{{qed}}
Theorem: Minimally Inductive Class under Progressing Mapping induces Nest

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$

Proof:
Let $\RR$ be the relation on $M$ defined as:
:$\forall x, y \in M: \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}}
From the Double Induction Principle, if $\RR$ is a relation on $M$ which satisfies:
{{begin-axiom}}
{{axiom | n = \text D_1
        | q = \forall x \in M
        | m = \map \RR {x, \O}
}}
{{axiom | n = \text D_2
        | q = \forall x, y \in M
        | 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 M$.
Thus:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
follows directly.
{{qed|lemma}}
Then the fact that:
:$\map g x \subseteq y \lor y \subseteq x$
implies that:
:$x \subseteq y \lor y \subseteq x$
because:
:$x \subseteq \map g x$
Hence the result by definition of a nest.
{{qed}}
Theorem: Minimally Inductive Class under Progressing Mapping induces Nest

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then $M$ is a nest in which:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$

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 induces Nest.
{{qed}}
Theorem: Sandwich Principle

Let $A$ be a class.
Let $g: A \to A$ be a mapping on $A$ such that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Then:
:$\forall x, y \in A: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, there is no element $y$ of $A$ such that:
:$x \subset y \subset \map g x$
where $\subset$ denotes a proper subset.

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: Sandwich Principle

Let $A$ be a class.
Let $g: A \to A$ be a mapping on $A$ such that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Then:
:$\forall x, y \in A: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, there is no element $y$ of $A$ such that:
:$x \subset y \subset \map g x$
where $\subset$ denotes a proper subset.

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: Sandwich Principle

Let $A$ be a class.
Let $g: A \to A$ be a mapping on $A$ such that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Then:
:$\forall x, y \in A: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, there is no element $y$ of $A$ such that:
:$x \subset y \subset \map g x$
where $\subset$ denotes a proper subset.

Proof:
We are given that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Let $x, y \in A$ such that:
:$x \subseteq y \subseteq \map g x$
{{AimForCont}} both $x \subset y$ and $y \subset \map g x$.
From $x \subset y$, it follows by definition of proper subset that:
:$\exists a \in y: a \notin x$
and so it is not the case that $y \subseteq x$.
From $y \subset \map g x$, it follows by definition of proper subset that:
:$\exists b \in \map g x: b \notin y$
and so it is not the case that $\map g x \subseteq y$.
Hence neither $y \subseteq x$ nor $\map g x \subseteq y$.
This contradicts the property of $g$.
Hence by Proof by Contradiction it follows that $y \subset \map g x$ and $x \subset y$ cannot both be true.
Therefore either $x = y$ or $y = \map g x$.
Hence the result.
{{Qed}}
Theorem: Sandwich Principle

Let $A$ be a class.
Let $g: A \to A$ be a mapping on $A$ such that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Then:
:$\forall x, y \in A: x \subseteq y \subseteq \map g x \implies x = y \lor y = \map g x$
That is, there is no element $y$ of $A$ such that:
:$x \subset y \subset \map g x$
where $\subset$ denotes a proper subset.

Proof:
We are given that:
:for all $x, y \in A$, either $\map g x \subseteq y$ or $y \subseteq x$.
Let $x, y \in A$ such that:
:$x \subseteq y \subseteq \map g x$
Then either we have:
:$\map g x \subseteq y$ and $y \subseteq \map g x$
in which case, by definition of set equality:
:$y = \map g x$
or we have that:
:$x \subseteq y$ and $y \subseteq x$
in which case, by definition of set equality:
:$x = y$
Thus either $y = \map g x$ or $x = y$ and the result follows.
{{Qed}}
Theorem: Sandwich Principle/Corollary 1

Let:
:$x \subset y$
where $\subset$ denotes a proper subset.
Then:
:$\map g x \subseteq y$

Proof:
Let $x \subset y$.
By hypothesis, either $\map g x \subseteq y$ or $y \subseteq x$.
But because $x \subset y$, it follows that $y \subseteq x$ cannot be the case.
Hence the result.
{{Qed}}
Theorem: Sandwich Principle/Corollary 2

Let $g$ be a progressing mapping.
Let $x \subseteq y$.
Then:
:$\map g x \subseteq \map g y$

Proof:
Let $x \subseteq y$.
Suppose $x = y$.
Then $\map g x \subseteq \map g y$ and the result holds.
{{qed|lemma}}
Suppose that $x \ne y$.
Then $x \subset y$
It follows from {{Corollary|Sandwich Principle|1}} that:
:$\map g x \subseteq y$
As $g$ is a progressing mapping on $A$:
:$y \subseteq \map g y$
Hence by Subset Relation is Transitive:
:$\map g x \subseteq \map g y$
{{qed|lemma}}
So in either case:
:$\map g x \subseteq \map g y$
{{Qed}}