Set which is Superinductive under Progressing Mapping has Fixed Point/Corollary

From ProofWiki
Jump to navigation Jump to search

Corollary to Set which is Superinductive under Progressing Mapping has Fixed Point

Let $S$ be a non-empty set of sets.

Let $g: S \to S$ be a progressing mapping on $S$ such that:

$(1): \quad S$ is closed under $g$
$(2): \quad S$ is closed under chain unions.

Let $b \in S$.

Then there exists $x \in S$ such that:

$b \subseteq x$

and:

$\map g x = x$


Proof

Let us assume the hypothesis.

Case $b = \O$

This case reduces to Set which is Superinductive under Progressing Mapping has Fixed Point.

Hence the result follows for $b = \O$.

$\Box$


Case $b \ne \O$

Let $S_b$ be the set of all elements $x$ of $S$ such that $b \subseteq x$, together with $\O$:

$S_b = \set {x \in S: b \subseteq x} \cup \set \O$

It is clear by inspection that $S_b$ is closed under chain unions.


Let us define the mapping $g': S_b \to S_b$ as follows:

$\forall x \in S_b: \map {g'} x = \begin{cases} b & : x = \O \\ \map g x & : x \ne \O \end{cases}$

Then:

$g'$ is a progressing mapping on $S_b$
$S_b$ is closed under $g'$
$\O \in S_b$

So $S_b$ is superinductive under $g'$.

Hence by Set which is Superinductive under Progressing Mapping has Fixed Point:

$\exists x \in S_b: x = \map {g'} x$

For such an $x$ we have that $x \ne \O$ because $\map {g'} \O = b$.

Hence:

$b \subseteq x$

Also because $x \ne \O$:

$\map {g'} x = \map g x$

and so:

$\map g x = x$

Hence:

$b \subseteq x$

and:

$\map g x = x$

and the proof is complete.

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Set_which_is_Superinductive_under_Progressing_Mapping_has_Fixed_Point/Corollary&oldid=582945"