Set of Subsets of Element of Minimally Inductive Class under Progressing Mapping is Finite

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.

Let $x \in M$.

Let $S$ be the set of all $y \in M$ such that $y \subseteq x$.


Then $S$ is finite.


Proof

The proof proceeds by general induction.

For all $x \in M$, let $\map P x$ be the proposition:

$\set {y \in M: y \subseteq x}$ is finite.


Basis for the Induction

We have that:

$\set {y \in M: y \subseteq \O} = \O$

From Cardinality of Empty Set, $\O$ is finite.

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:

$\set {y \in M: y \subseteq x}$ is finite.


from which it is to be shown that:

$\set {y \in M: y \subseteq \map g x}$ is finite.


Induction Step

This is the induction step:

Let $S = \set {y \in M: y \subseteq x}$.

By the induction hypothesis, $S$ is finite.


Consider the set:

$S' = \set {y \in M: y \subseteq \map g x}$

By definition of progressing mapping:

$x \subseteq \map g x$

Hence it follows that:

$S \subseteq S'$


Let $y \in S' \setminus S$.

Then:

$y \notin S$

and so:

$y \nsubseteq x$

From Minimally Inductive Class under Progressing Mapping induces Nest:

$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$

As it is not the case that $y \subseteq x$, it must be that:

$\map g x \subseteq y$

From sandwich principle:

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

As $x \ne y$ (or then $y \subseteq x$), it must be the case that:

$y = \map g x$

So:

$S' \setminus S = \map g x$

and so is finite, containing $1$ element.

We have that:

$S' = S \cup \paren {S' \setminus S}$

and it follows from Union of Finite Sets is Finite that $S'$ is finite.


So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.


Therefore:

$\forall x \in M: \set {y \in M: y \subseteq x}$ is finite.


Sources