IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Finite_ZF imports ZF1 Nat_ZF_IML ZF.Cardinal
begin

Standard Isabelle Finite.thy contains a very useful notion of finite powerset: the set of finite subsets of a given set. The definition, however, is specific to Isabelle and based on the notion of "datatype", obviously not something that belongs to ZF set theory. This theory file devolops the notion of finite powerset similarly as in Finite.thy, but based on standard library's Cardinal.thy. This theory file is intended to replace IsarMathLib's Finite1 and Finite_ZF_1 theories that are currently derived from the "datatype" approach.

Definition and basic properties of finite powerset

The goal of this section is to prove an induction theorem about finite powersets: if the empty set has some property and this property is preserved by adding a single element of a set, then this property is true for all finite subsets of this set.

We defined the finite powerset \( \text{FinPow}(X) \) as those elements of the powerset that are finite.

definition

\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)

The cardinality of an element of finite powerset is a natural number.

lemma card_fin_is_nat:

assumes \( A \in \text{FinPow}(X) \)

shows \( |A| \in nat \) and \( A \approx |A| \) using assms, FinPow_def, Finite_def, cardinal_cong, nat_into_Card, Card_cardinal_eq

A reformulation of card_fin_is_nat: for a finit set \(A\) there is a bijection between \(|A|\) and \(A\).

lemma fin_bij_card:

assumes A1: \( A \in \text{FinPow}(X) \)

shows \( \exists b.\ b \in \text{bij}(|A|, A) \)proof
from A1 have \( |A| \approx A \) using card_fin_is_nat, eqpoll_sym
then show \( thesis \) using eqpoll_def
qed

If a set has the same number of elements as \(n \in \mathbb{N}\), then its cardinality is \(n\). Recall that in set theory a natural number \(n\) is a set that has \(n\) elements.

lemma card_card:

assumes \( A \approx n \) and \( n \in nat \)

shows \( |A| = n \) using assms, cardinal_cong, nat_into_Card, Card_cardinal_eq

If we add a point to a finite set, the cardinality increases by one. To understand the second assertion \(| A \cup \{ a\}| = |A| \cup \{ |A|\} \) recall that the cardinality \(|A|\) of \(A\) is a natural number and for natural numbers we have \(n+1 = n \cup \{ n\}\).

lemma card_fin_add_one:

assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( a \in X-A \)

shows \( |A \cup \{a\}| = succ( |A| ) \), \( |A \cup \{a\}| = |A| \cup \{|A|\} \)proof
from A1, A2 have \( cons(a,A) \approx cons( |A|, |A| ) \) using card_fin_is_nat, mem_not_refl, cons_eqpoll_cong
moreover
have \( cons(a,A) = A \cup \{a\} \) by (rule consdef )
moreover
have \( cons( |A|, |A| ) = |A| \cup \{|A|\} \) by (rule consdef )
ultimately have \( A\cup \{a\} \approx succ( |A| ) \) using succ_explained
with A1 show \( |A \cup \{a\}| = succ( |A| ) \) and \( |A \cup \{a\}| = |A| \cup \{|A|\} \) using card_fin_is_nat, card_card
qed

We can decompose the finite powerset into collection of sets of the same natural cardinalities.

lemma finpow_decomp:

shows \( \text{FinPow}(X) = (\bigcup n \in nat.\ \{A \in Pow(X).\ A \approx n\}) \) using Finite_def, FinPow_def

Finite powerset is the union of sets of cardinality bounded by natural numbers.

lemma finpow_union_card_nat:

shows \( \text{FinPow}(X) = (\bigcup n \in nat.\ \{A \in Pow(X).\ A \preceq n\}) \)proof
have \( \text{FinPow}(X) \subseteq (\bigcup n \in nat.\ \{A \in Pow(X).\ A \preceq n\}) \) using finpow_decomp, FinPow_def, eqpoll_imp_lepoll
moreover
have \( (\bigcup n \in nat.\ \{A \in Pow(X).\ A \preceq n\}) \subseteq \text{FinPow}(X) \) using lepoll_nat_imp_Finite, FinPow_def
ultimately show \( thesis \)
qed

A different form of finpow_union_card_nat (see above) - a subset that has not more elements than a given natural number is in the finite powerset.

lemma lepoll_nat_in_finpow:

assumes \( n \in nat \), \( A \subseteq X \), \( A \preceq n \)

shows \( A \in \text{FinPow}(X) \) using assms, finpow_union_card_nat

Natural numbers are finite subsets of the set of natural numbers.

lemma nat_finpow_nat:

assumes \( n \in nat \)

shows \( n \in \text{FinPow}(nat) \) using assms, nat_into_Finite, nat_subset_nat, FinPow_def

A finite subset is a finite subset of itself.

lemma fin_finpow_self:

assumes \( A \in \text{FinPow}(X) \)

shows \( A \in \text{FinPow}(A) \) using assms, FinPow_def

If we remove an element and put it back we get the set back.

lemma rem_add_eq:

assumes \( a\in A \)

shows \( (A-\{a\}) \cup \{a\} = A \) using assms

Induction for finite powerset. This is smilar to the standard Isabelle's Fin_induct.

theorem FinPow_induct:

assumes A1: \( P(0) \) and A2: \( \forall A \in \text{FinPow}(X).\ P(A) \longrightarrow (\forall a\in X.\ P(A \cup \{a\})) \) and A3: \( B \in \text{FinPow}(X) \)

shows \( P(B) \)proof
{
fix \( n \)
assume \( n \in nat \)
moreover
from A1 have I: \( \forall B\in Pow(X).\ B \preceq 0 \longrightarrow P(B) \) using lepoll_0_is_0
moreover
have \( \forall k \in nat.\ \) \( (\forall B \in Pow(X).\ (B \preceq k \longrightarrow P(B))) \longrightarrow \) \( (\forall B \in Pow(X).\ (B \preceq succ(k) \longrightarrow P(B))) \)proof
{
fix \( k \)
assume A4: \( k \in nat \)
assume A5: \( \forall B \in Pow(X).\ (B \preceq k \longrightarrow P(B)) \)
fix \( B \)
assume A6: \( B \in Pow(X) \), \( B \preceq succ(k) \)
have \( P(B) \)proof
have \( B = 0 \longrightarrow P(B) \)proof
{
assume \( B = 0 \)
then have \( B \preceq 0 \) using lepoll_0_iff
with I, A6 have \( P(B) \)
}
thus \( B = 0 \longrightarrow P(B) \)
qed
moreover
have \( B\neq 0 \longrightarrow P(B) \)proof
{
assume \( B \neq 0 \)
then obtain \( a \) where II: \( a\in B \)
let \( A = B - \{a\} \)
from A6, II have \( A \subseteq X \) and \( A \preceq k \) using Diff_sing_lepoll
with A4, A5 have \( A \in \text{FinPow}(X) \) and \( P(A) \) using lepoll_nat_in_finpow, finpow_decomp
with A2, A6, II have \( P(A \cup \{a\}) \)
moreover
from II have \( A \cup \{a\} = B \)
ultimately have \( P(B) \)
}
thus \( B\neq 0 \longrightarrow P(B) \)
qed
ultimately show \( P(B) \)
qed
}
thus \( thesis \)
qed
ultimately have \( \forall B \in Pow(X).\ (B \preceq n \longrightarrow P(B)) \) by (rule ind_on_nat )
}
then have \( \forall n \in nat.\ \forall B \in Pow(X).\ (B \preceq n \longrightarrow P(B)) \)
with A3 show \( P(B) \) using finpow_union_card_nat
qed

A subset of a finite subset is a finite subset.

lemma subset_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \subseteq A \)

shows \( B \in \text{FinPow}(X) \) using assms, FinPow_def, subset_Finite

If we subtract anything from a finite set, the resulting set is finite.

lemma diff_finpow:

assumes \( A \in \text{FinPow}(X) \)

shows \( A-B \in \text{FinPow}(X) \) using assms, subset_finpow

If we remove a point from a finites subset, we get a finite subset.

corollary fin_rem_point_fin:

assumes \( A \in \text{FinPow}(X) \)

shows \( A - \{a\} \in \text{FinPow}(X) \) using assms, diff_finpow

Cardinality of a nonempty finite set is a successsor of some natural number.

lemma card_non_empty_succ:

assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( A \neq 0 \)

shows \( \exists n \in nat.\ |A| = succ(n) \)proof
from A2 obtain \( a \) where \( a \in A \)
let \( B = A - \{a\} \)
from A1, \( a \in A \) have \( B \in \text{FinPow}(X) \) and \( a \in X - B \) using FinPow_def, fin_rem_point_fin
then have \( |B \cup \{a\}| = succ( |B| ) \) using card_fin_add_one
moreover
from \( a \in A \), \( B \in \text{FinPow}(X) \) have \( A = B \cup \{a\} \) and \( |B| \in nat \) using card_fin_is_nat
ultimately show \( \exists n \in nat.\ |A| = succ(n) \)
qed

Nonempty set has non-zero cardinality. This is probably true without the assumption that the set is finite, but I couldn't derive it from standard Isabelle theorems.

lemma card_non_empty_non_zero:

assumes \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)

shows \( |A| \neq 0 \)proof
from assms obtain \( n \) where \( |A| = succ(n) \) using card_non_empty_succ
then show \( |A| \neq 0 \) using succ_not_0
qed

Another variation on the induction theme: If we can show something holds for the empty set and if it holds for all finite sets with at most \(k\) elements then it holds for all finite sets with at most \(k+1\) elements, the it holds for all finite sets.

theorem FinPow_card_ind:

assumes A1: \( P(0) \) and A2: \( \forall k\in nat.\ \) \( (\forall A \in \text{FinPow}(X).\ A \preceq k \longrightarrow P(A)) \longrightarrow \) \( (\forall A \in \text{FinPow}(X).\ A \preceq succ(k) \longrightarrow P(A)) \) and A3: \( A \in \text{FinPow}(X) \)

shows \( P(A) \)proof
from A3 have \( |A| \in nat \) and \( A \in \text{FinPow}(X) \) and \( A \preceq |A| \) using card_fin_is_nat, eqpoll_imp_lepoll
moreover
have \( \forall n \in nat.\ (\forall A \in \text{FinPow}(X).\ \) \( A \preceq n \longrightarrow P(A)) \)proof
fix \( n \)
assume \( n \in nat \)
moreover
from A1 have \( \forall A \in \text{FinPow}(X).\ A \preceq 0 \longrightarrow P(A) \) using lepoll_0_is_0
moreover
note A2
ultimately show \( \forall A \in \text{FinPow}(X).\ A \preceq n \longrightarrow P(A) \) by (rule ind_on_nat )
qed
ultimately show \( P(A) \)
qed

Another type of induction (or, maybe recursion). In the induction step we try to find a point in the set that if we remove it, the fact that the property holds for the smaller set implies that the property holds for the whole set.

lemma FinPow_ind_rem_one:

assumes A1: \( P(0) \) and A2: \( \forall A \in \text{FinPow}(X).\ A \neq 0 \longrightarrow (\exists a\in A.\ P(A-\{a\}) \longrightarrow P(A)) \) and A3: \( B \in \text{FinPow}(X) \)

shows \( P(B) \)proof
note A1
moreover
have \( \forall k\in nat.\ \) \( (\forall B \in \text{FinPow}(X).\ B \preceq k \longrightarrow P(B)) \longrightarrow \) \( (\forall C \in \text{FinPow}(X).\ C \preceq succ(k) \longrightarrow P(C)) \)proof
{
fix \( k \)
assume \( k \in nat \)
assume A4: \( \forall B \in \text{FinPow}(X).\ B \preceq k \longrightarrow P(B) \)
have \( \forall C \in \text{FinPow}(X).\ C \preceq succ(k) \longrightarrow P(C) \)proof
{
fix \( C \)
assume \( C \in \text{FinPow}(X) \)
assume \( C \preceq succ(k) \)
note A1
moreover {
assume \( C \neq 0 \)
with A2, \( C \in \text{FinPow}(X) \) obtain \( a \) where \( a\in C \) and \( P(C-\{a\}) \longrightarrow P(C) \)
with A4, \( C \in \text{FinPow}(X) \), \( C \preceq succ(k) \) have \( P(C) \) using Diff_sing_lepoll, fin_rem_point_fin
} ultimately have \( P(C) \)
}
thus \( thesis \)
qed
}
thus \( thesis \)
qed
moreover
note A3
ultimately show \( P(B) \) by (rule FinPow_card_ind )
qed

Yet another induction theorem. This is similar, but slightly more complicated than FinPow_ind_rem_one. The difference is in the treatment of the empty set to allow to show properties that are not true for empty set.

lemma FinPow_rem_ind:

assumes A1: \( \forall A \in \text{FinPow}(X).\ \) \( A = 0 \vee (\exists a\in A.\ A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A)) \) and A2: \( A \in \text{FinPow}(X) \) and A3: \( A\neq 0 \)

shows \( P(A) \)proof
have \( 0 = 0 \vee P(0) \)
moreover
have \( \forall k\in nat.\ \) \( (\forall B \in \text{FinPow}(X).\ B \preceq k \longrightarrow (B=0 \vee P(B))) \longrightarrow \) \( (\forall A \in \text{FinPow}(X).\ A \preceq succ(k) \longrightarrow (A=0 \vee P(A))) \)proof
{
fix \( k \)
assume \( k \in nat \)
assume A4: \( \forall B \in \text{FinPow}(X).\ B \preceq k \longrightarrow (B=0 \vee P(B)) \)
have \( \forall A \in \text{FinPow}(X).\ A \preceq succ(k) \longrightarrow (A=0 \vee P(A)) \)proof
{
fix \( A \)
assume \( A \in \text{FinPow}(X) \)
assume \( A \preceq succ(k) \), \( A\neq 0 \)
from A1, \( A \in \text{FinPow}(X) \), \( A\neq 0 \) obtain \( a \) where \( a\in A \) and \( A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A) \)
let \( B = A-\{a\} \)
from A4, \( A \in \text{FinPow}(X) \), \( A \preceq succ(k) \), \( a\in A \) have \( B = 0 \vee P(B) \) using Diff_sing_lepoll, fin_rem_point_fin
with \( a\in A \), \( A = \{a\} \vee P(A-\{a\}) \longrightarrow P(A) \) have \( P(A) \)
}
thus \( thesis \)
qed
}
thus \( thesis \)
qed
moreover
note A2
ultimately have \( A=0 \vee P(A) \) by (rule FinPow_card_ind )
with A3 show \( P(A) \)
qed

If a family of sets is closed with respect to taking intersections of two sets then it is closed with respect to taking intersections of any nonempty finite collection.

lemma inter_two_inter_fin:

assumes A1: \( \forall V\in T.\ \forall W\in T.\ V \cap W \in T \) and A2: \( N \neq 0 \) and A3: \( N \in \text{FinPow}(T) \)

shows \( (\bigcap N \in T) \)proof
have \( 0 = 0 \vee (\bigcap 0 \in T) \)
moreover
have \( \forall M \in \text{FinPow}(T).\ (M = 0 \vee \bigcap M \in T) \longrightarrow \) \( (\forall W \in T.\ M\cup \{W\} = 0 \vee \bigcap (M \cup \{W\}) \in T) \)proof
{
fix \( M \)
assume \( M \in \text{FinPow}(T) \)
assume A4: \( M = 0 \vee \bigcap M \in T \)
{
assume \( M = 0 \)
hence \( \forall W \in T.\ M\cup \{W\} = 0 \vee \bigcap (M \cup \{W\}) \in T \)
}
moreover {
assume \( M \neq 0 \)
with A4 have \( \bigcap M \in T \)
{
fix \( W \)
assume \( W \in T \)
from \( M \neq 0 \) have \( \bigcap (M \cup \{W\}) = (\bigcap M) \cap W \)
with A1, \( \bigcap M \in T \), \( W \in T \) have \( \bigcap (M \cup \{W\}) \in T \)
}
hence \( \forall W \in T.\ M\cup \{W\} = 0 \vee \bigcap (M \cup \{W\}) \in T \)
} ultimately have \( \forall W \in T.\ M\cup \{W\} = 0 \vee \bigcap (M \cup \{W\}) \in T \)
}
thus \( thesis \)
qed
moreover
note \( N \in \text{FinPow}(T) \)
ultimately have \( N = 0 \vee (\bigcap N \in T) \) by (rule FinPow_induct )
with A2 show \( (\bigcap N \in T) \)
qed

If a family of sets contains the empty set and is closed with respect to taking unions of two sets then it is closed with respect to taking unions of any finite collection.

lemma union_two_union_fin:

assumes A1: \( 0 \in C \) and A2: \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) and A3: \( N \in \text{FinPow}(C) \)

shows \( \bigcup N \in C \)proof
from \( 0 \in C \) have \( \bigcup 0 \in C \)
moreover
have \( \forall M \in \text{FinPow}(C).\ \bigcup M \in C \longrightarrow (\forall A\in C.\ \bigcup (M \cup \{A\}) \in C) \)proof
{
fix \( M \)
assume \( M \in \text{FinPow}(C) \)
assume \( \bigcup M \in C \)
fix \( A \)
assume \( A\in C \)
have \( \bigcup (M \cup \{A\}) = (\bigcup M) \cup A \)
with A2, \( \bigcup M \in C \), \( A\in C \) have \( \bigcup (M \cup \{A\}) \in C \)
}
thus \( thesis \)
qed
moreover
note \( N \in \text{FinPow}(C) \)
ultimately show \( \bigcup N \in C \) by (rule FinPow_induct )
qed

Empty set is in finite power set.

lemma empty_in_finpow:

shows \( 0 \in \text{FinPow}(X) \) using FinPow_def

Singleton is in the finite powerset.

lemma singleton_in_finpow:

assumes \( x \in X \)

shows \( \{x\} \in \text{FinPow}(X) \) using assms, FinPow_def

Union of two finite subsets is a finite subset.

lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \) using assms, FinPow_def

Union of finite number of finite sets is finite.

lemma fin_union_finpow:

assumes \( M \in \text{FinPow}( \text{FinPow}(X)) \)

shows \( \bigcup M \in \text{FinPow}(X) \) using assms, empty_in_finpow, union_finpow, union_two_union_fin

If a set is finite after removing one element, then it is finite.

lemma rem_point_fin_fin:

assumes A1: \( x \in X \) and A2: \( A - \{x\} \in \text{FinPow}(X) \)

shows \( A \in \text{FinPow}(X) \)proof
from assms have \( (A - \{x\}) \cup \{x\} \in \text{FinPow}(X) \) using singleton_in_finpow, union_finpow
moreover
have \( A \subseteq (A - \{x\}) \cup \{x\} \)
ultimately show \( A \in \text{FinPow}(X) \) using FinPow_def, subset_Finite
qed

An image of a finite set is finite.

lemma fin_image_fin:

assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)proof
have \( \{K(V).\ V\in 0\} \in \text{FinPow}(C) \) using FinPow_def
moreover
have \( \forall A \in \text{FinPow}(B).\ \) \( \{K(V).\ V\in A\} \in \text{FinPow}(C) \longrightarrow (\forall a\in B.\ \{K(V).\ V \in (A \cup \{a\})\} \in \text{FinPow}(C)) \)proof
{
fix \( A \)
assume \( A \in \text{FinPow}(B) \)
assume \( \{K(V).\ V\in A\} \in \text{FinPow}(C) \)
fix \( a \)
assume \( a\in B \)
have \( \{K(V).\ V \in (A \cup \{a\})\} \in \text{FinPow}(C) \)proof
have \( \{K(V).\ V \in (A \cup \{a\})\} = \{K(V).\ V\in A\} \cup \{K(a)\} \)
moreover
note \( \{K(V).\ V\in A\} \in \text{FinPow}(C) \)
moreover
from \( \forall V\in B.\ K(V) \in C \), \( a\in B \) have \( \{K(a)\} \in \text{FinPow}(C) \) using singleton_in_finpow
ultimately show \( thesis \) using union_finpow
qed
}
thus \( thesis \)
qed
moreover
note \( N \in \text{FinPow}(B) \)
ultimately show \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \) by (rule FinPow_induct )
qed

Union of a finite indexed family of finite sets is finite.

lemma union_fin_list_fin:

assumes A1: \( n \in nat \) and A2: \( \forall k \in n.\ N(k) \in \text{FinPow}(X) \)

shows \( \{N(k).\ k \in n\} \in \text{FinPow}( \text{FinPow}(X)) \) and \( (\bigcup k \in n.\ N(k)) \in \text{FinPow}(X) \)proof
from A1 have \( n \in \text{FinPow}(n) \) using nat_finpow_nat, fin_finpow_self
with A2 show \( \{N(k).\ k \in n\} \in \text{FinPow}( \text{FinPow}(X)) \) by (rule fin_image_fin )
then show \( (\bigcup k \in n.\ N(k)) \in \text{FinPow}(X) \) using fin_union_finpow
qed
end
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma card_fin_is_nat:

assumes \( A \in \text{FinPow}(X) \)

shows \( |A| \in nat \) and \( A \approx |A| \)
lemma consdef: shows \( cons(a,A) = A \cup \{a\} \)
lemma succ_explained: shows \( succ(n) = n \cup \{n\} \)
lemma card_card:

assumes \( A \approx n \) and \( n \in nat \)

shows \( |A| = n \)
lemma finpow_decomp: shows \( \text{FinPow}(X) = (\bigcup n \in nat.\ \{A \in Pow(X).\ A \approx n\}) \)
lemma finpow_union_card_nat: shows \( \text{FinPow}(X) = (\bigcup n \in nat.\ \{A \in Pow(X).\ A \preceq n\}) \)
lemma nat_subset_nat:

assumes \( n \in nat \)

shows \( n \subseteq nat \)
lemma lepoll_nat_in_finpow:

assumes \( n \in nat \), \( A \subseteq X \), \( A \preceq n \)

shows \( A \in \text{FinPow}(X) \)
theorem ind_on_nat:

assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(succ(k)) \)

shows \( P(n) \)
lemma subset_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \subseteq A \)

shows \( B \in \text{FinPow}(X) \)
lemma diff_finpow:

assumes \( A \in \text{FinPow}(X) \)

shows \( A-B \in \text{FinPow}(X) \)
corollary fin_rem_point_fin:

assumes \( A \in \text{FinPow}(X) \)

shows \( A - \{a\} \in \text{FinPow}(X) \)
lemma card_fin_add_one:

assumes \( A \in \text{FinPow}(X) \) and \( a \in X-A \)

shows \( |A \cup \{a\}| = succ( |A| ) \), \( |A \cup \{a\}| = |A| \cup \{|A|\} \)
lemma card_non_empty_succ:

assumes \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)

shows \( \exists n \in nat.\ |A| = succ(n) \)
theorem FinPow_card_ind:

assumes \( P(0) \) and \( \forall k\in nat.\ \) \( (\forall A \in \text{FinPow}(X).\ A \preceq k \longrightarrow P(A)) \longrightarrow \) \( (\forall A \in \text{FinPow}(X).\ A \preceq succ(k) \longrightarrow P(A)) \) and \( A \in \text{FinPow}(X) \)

shows \( P(A) \)
theorem FinPow_induct:

assumes \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ P(A) \longrightarrow (\forall a\in X.\ P(A \cup \{a\})) \) and \( B \in \text{FinPow}(X) \)

shows \( P(B) \)
lemma empty_in_finpow: shows \( 0 \in \text{FinPow}(X) \)
lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)
lemma union_two_union_fin:

assumes \( 0 \in C \) and \( \forall A\in C.\ \forall B\in C.\ A\cup B \in C \) and \( N \in \text{FinPow}(C) \)

shows \( \bigcup N \in C \)
lemma singleton_in_finpow:

assumes \( x \in X \)

shows \( \{x\} \in \text{FinPow}(X) \)
lemma nat_finpow_nat:

assumes \( n \in nat \)

shows \( n \in \text{FinPow}(nat) \)
lemma fin_finpow_self:

assumes \( A \in \text{FinPow}(X) \)

shows \( A \in \text{FinPow}(A) \)
lemma fin_image_fin:

assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)
lemma fin_union_finpow:

assumes \( M \in \text{FinPow}( \text{FinPow}(X)) \)

shows \( \bigcup M \in \text{FinPow}(X) \)